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

At: length wf nat 1 1
1. T: Type
2. L: T List
3. u: T
4. v: T List
5. ||v||

0||v||+1
By: GenConcl (||v|| = n)
Generated subgoals:

None

About:
listnatural_numberadduniverseequalmember

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