type 'a list = Nil | Cons of 'a * 'a list type 'a ntree = NLeaf | NNode of 'a ntree * 'a * 'a ntree let rec spine : forall 'a. 'a ntree -> 'a list = fun ['a] (t : 'a ntree) => match t with | NLeaf => Nil['a] | NNode(l,x,r) => Cons['a](x, spine ['a] l) end let forall 'a ornament spine ['a] : 'a ntree -> 'a list