theorem lmemS (a b l: nat): $ a IN b : l <-> a = b \/ a IN l $;
Step | Hyp | Ref | Expression |
---|---|---|---|
2 |
lmems (b : l) = b ; lmems l -> (a e. lmems (b : l) <-> a e. b ; lmems l) |
||
3 |
conv lmem |
lmems (b : l) = b ; lmems l -> (a IN b : l <-> a e. b ; lmems l) |
|
4 |
lmems (b : l) = b ; lmems l |
||
5 |
a IN b : l <-> a e. b ; lmems l |
||
7 |
a e. b ; lmems l <-> a = b \/ a e. lmems l |
||
8 |
conv lmem |
a e. b ; lmems l <-> a = b \/ a IN l |
|
9 |
bitr* |
a IN b : l <-> a = b \/ a IN l |