1
Inductive List (A : Set) : Set :=
3
| Cons : A -> List A -> List A.
5
Inductive Empty (A : Set) : List A -> Prop :=
6
intro_Empty : Empty A (Nil A).
9
inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x).
13
(fun (A : Set) (l : List A) =>
14
match l return (Empty A l \/ ~ Empty A l) with
15
| Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A)
16
| Cons a y as b => or_intror (Empty A b) (inv_Empty A a y)