\ / GNU General Public License Version 2
V_______________________________________________________________ *)
+include "basics/core_notation/pair_2.ma".
include "basics/logic.ma".
(* void *)
(* 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] ≝ {