definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
-lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → ⊥.
+lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
(∀v. x = Some ? v → Q (P v)) →
Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
#A #B #P #Q *
(* sigma *)
record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
- pi1: A
+ pi1: A (* not a coercion due to problems with Cerco *)
; pi2: f pi1
}.
#A #P #P' #H1 * #x #H2 @H1 @H2
qed.
+lemma inj_mk_Sig: ∀A,P.∀x. x = mk_Sig A P (pi1 A P x) (pi2 A P x).
+#A #P #x cases x //
+qed-.
(* Prod *)
record Prod (A,B:Type[0]) : Type[0] ≝ {