right object 1 with ! end object; right object prod(a,b) with pair is pi1: prod -> a pi2: prod -> b end object; right object exp(a,b) with curry is eval: prod(exp,a) -> b end object; let uncurry(f) = eval . prod(f, I); left object nat with pr is 0: 1 -> nat s: nat -> nat end object; left object coprod(a,b) with case is in1: a -> coprod in2: b -> coprod end object; show pair(pi2,eval); let add=eval.prod(pr(curry(pi2), curry(s.eval)), I); simp add.pair(s.s.0, s.0); let mult=eval.prod(pr(curry(0.!), curry(add.pair(eval, pi2))), I); let primrec(f,g) = pi2.pr(pair(0,f), pair(s.pi1, g)); let fact = primrec(s.0, mult.prod(s,I)); simp fact.s.s.s.s.0; left object list(p) with prl is nil: 1 -> list cons: prod(p,list) -> list end object; let append = eval.prod(prl(curry(pi2), curry(cons.pair(pi1.pi1, eval.pair(pi2.pi1, pi2)))), I); let reverse=prl(nil, append.pair(pi2, cons.pair(pi1, nil.!))); let hd = prl(in2, in1.pi1); let hdp=case(hd,in2); let tl = coprod(pi2,I).prl(in2, in1.prod(I, case(cons,nil))); let tlp = case(tl, in2); let seq = pi2.pr(pair(0,nil), pair(s.pi1, cons)); simp seq.s.s.s.0; simp full seq.s.s.s.0; simp hdp.tl.seq.s.s.s.0; simp full append.pair(seq.s.s.0, seq.s.s.s.0); simp full reverse.it; right object inflist(a) with fold is head: inflist -> a tail: inflist -> inflist end object; let incseq=fold(I,s).0; simp head.incseq; simp head.tail.tail.tail.incseq; let alt=fold(head.pi1, pair(pi2, tail.pi1)); let infseq=fold(I,I).0; simp head.tail.tail.alt.pair(incseq, infseq); #exit;