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

At: list all is member nil lemma 1
1. T: Type
2. eq: TT
3. L: T List

xL.x(eq) nil nil = L
By: Analyze 3 THEN Rewrite (HigherC list_all_unrollC) 0 THENL [Auto;Analyze 0]
Generated subgoal:

14. u: T
5. v: T List
6. u(eq) nil & xv.x(eq) nil
nil = u.v

About:
listconsnilboolassertfunctionuniverseequalimplies

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