theorem lmemsnocid (a l: nat): $ a IN l |> a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmemsnoc | a IN l |> a <-> a IN l \/ a = a |
|
2 | orr | a = a -> a IN l \/ a = a |
|
3 | eqid | a = a |
|
4 | 2, 3 | ax_mp | a IN l \/ a = a |
5 | 1, 4 | mpbir | a IN l |> a |