1 2 3 4 5 6 7 8
Inductive List [A:Set] :Set := Nil:(List A) | Cons:A->(List A)->(List A). Type <nat>Cases (Nil nat) of ((Nil_) as b) =>b |((Cons _ _ _) as d) => d end.