(24steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

At: append is member lemma 1 1 1 1 1
1. T: Type
2. eq: {T=}
3. eq TT
4. x,y:T. eq(x,y) x = y
5. L: T List
6. x: T
7. M: T List
8. N: T List

nil = (nil @ (x.N)) False
By:
AbReduce 0
THEN
Analyze 0
Generated subgoal:

19. nil = x.N
False

About:
listconsnilboolassertapplyfunction
universeequalmemberimpliesfalse
all

(24steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc