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

At: length wf nat 1
1. T: Type
2. L: T List

||L||
By:
ListInd 2
THEN
Reduce 0
Generated subgoal:

13. u: T
4. v: T List
5. ||v||
0||v||+1

About:
listnatural_numberadduniversemember

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