blob: 6e2aea480a49a568adfb55040145fd8ae70f4567 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Inductive List [A:Set] :Set :=
Nil:(List A) | Cons:A->(List A)->(List A).
Inductive Empty [A:Set] : (List A)-> Prop :=
intro_Empty: (Empty A (Nil A)).
Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)).
Type
[A:Set]
[l:(List A)]
<[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of
Nil => (or_introl ? ~(Empty A (Nil A)) (intro_Empty A))
| ((Cons a y) as b) => (or_intror (Empty A b) ? (inv_Empty A a y))
end.
|
