right object 1 with ! is
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;

left object nat with pr is
  0: 1 -> nat
  s: nat -> nat
end object;

let times=eval.prod(pr(curry(curry(pi2)), curry(curry(eval.pair(eval.pi1,eval.pair(pi2.pi1,pi2))))),I);
let ack_0=curry(s.pi2);
let ack_s=curry(eval.pair(times.pair(s.pi2,pi1),s.0.!));
let ack=eval.prod(pr(ack_0,ack_s),I);

simp full ack.pair(s.s.s.0, s.s.s.s.0);