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

At: list length non negative 2
1. T: Type
2. L: T List
3. u: T
4. v: T List
5. ||(v)0

1+||(v)0
By: Reduce 0
Generated subgoals:

None

About:
listnatural_numberaddapplyuniverse

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