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

At: list length wf int 1 1

1. T: Type

Y(l,L. Case of L; nil 0 ; h.t 1+l(t)) (T List)

By:
RWH YUnrollC 0
THEN
Reduce 0


Generated subgoal:

1 (L.Case of L; nil 0 ; h.t 1+Y((l,L. Case of L; nil 0 ; h.t 1+l(t)),t)) (T List)

About:
listlist_indint
natural_numberaddlambdaapplyfunctionycombuniverse
member

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