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

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

xnil.x(eq) nil
By:
Rewrite (HigherC list_all_unrollC) 0
THEN
Trivial
Generated subgoals:

None

About:
listnilboolassertfunctionuniverseequal

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