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

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

||(L)
By:
Analyze 2
THEN
Rewrite (HigherC list_length_unrollC) 0
Generated subgoals:

1 0
23. u: T
4. v: T List
1+||(v)

About:
listnatural_numberaddapplyuniversemember

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