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

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

xL.x(eq) nil
By: RevHypSubst 4 0
Generated subgoal:

1 xnil.x(eq) nil

About:
listnilboolassertfunctionuniverseequal

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