data I -> inflist(A) = head: I -> A | tail: I -> I. def nats: 1 -> inflist(nat) = () => (| n => head: n | tail: succ n |) zero. def array_nats: 1 -> inflist(inflist(nat)) = () => inflist{m => inflist{n => add (m, n)} nats} nats. def get_inflist: nat * inflist(A) -> A = (n, il) => head {| zero: () => il | succ: il' => tail il' |} n.