list a ::= Nil | Cons a (list a); quad a b c d ::= MkQuad a b c d; ;; bury x = MkQuad (Cons (Cons (Cons x Nil) Nil) Nil) (Cons (Cons (Cons x Nil) Nil) Nil) (Cons (Cons (Cons x Nil) Nil) Nil) (Cons (Cons (Cons x Nil) Nil) Nil);