| Cons of int * nlbody let isnil l = match l with Nil (_) -> true | Cons (_) -> false let hd l = match l with Nil (_) -> 0 | Cons (i1, _) -> i1 let tl l = match l with Nil (_) -> l | Cons (_, tl) -> tl NLBody = h nil : Unit, cons : { Nat, NatList }i nil = fold [ NatList ](h nil = unit i as NLBody cons = n : Nat. l : NatList. fold [ NatList ]h cons = { n, l }i as NLBody isnil = l : NatList. case unfold [ NatList ] l of h nil = u i ) true | h cons = p i ) false hd = l : NatList. case unfold [ NatList ] l of h nil = u i ) 0 | h cons = p i ) p. 1 tl = ...