interpretation "cons" 'cons hd tl = (cons ? hd tl).
definition is_nil: ∀A:Type[0].list A → Prop ≝
- λA.λl.match l with [ nil ⇒ ⊤ | cons hd tl ⇒ ⊥ ].
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
theorem nil_cons:
∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
match l with
-[ nil ⇒ ⊥
+[ nil ⇒ False
| cons h t ⇒ (P h) ∨ (Exists A P t)
].