var a: Type
type List a
op nil : List a
op head : List a -> a
op snoc: List a -> a --> List a
forall x:a
. snoc nil x = snoc nil x
. head nil x = x