'b,'a:S, x:'b, f:('b
'a('a List)'b).
Thm* (
fn1:(('a List)'b).
Thm* (fn1(nil) = x & (
h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t)))
Thm* & (
fn1,y:(('a List)'b).
Thm* & (fn1(nil) = x & (
h:'a, t:'a List. fn1(cons(h; t)) = f(fn1(t),h,t))
Thm* & (& y(nil) = x
Thm* & (& (
h:'a, t:'a List. y(cons(h; t)) = f(y(t),h,t))
Thm* & (
Thm* & (fn1 = y)
'b,'a:S.
Thm* all
Thm* (
x:'b. all
Thm* (
x:'b. (f:'b
Thm* (
x:'b. ( 'a
Thm* (
x:'b. ( hlist('a)
Thm* (
x:'b. ( 'b. exists_unique
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. and
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. (equal(fn1(nil),x)
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,all
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. all
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). equal
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). (fn1
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). ((cons(h,t))
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). ,f
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). ,(fn1(t)
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). ,,h
Thm* (
x:'b. ( 'b. (fn1:hlist('a) 'b. ,(h:'a. (t:hlist('a). ,,t))))))))