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

At: list length non negative

T:Type, L:T List. ||(L)0
By:
UnivCD
THEN
ListInd 2
THEN
AbReduce 0
Generated subgoals:

11. T: Type
2. L: T List
00
21. T: Type
2. L: T List
3. u: T
4. v: T List
5. ||(v)0
1+||(v)0

About:
listnatural_numberaddapplyuniverseall

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