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

At: apply wf list length int 1 2
1. T: Type
2. L: T List
3. u: T
4. v: T List

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

None

About:
listintnatural_numberaddapplyuniverseequalmember

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