(* dependent pair *)
record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
- dpi1: A
+ dpi1:> A
; dpi2: f dpi1
}.
interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
+lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' (pi1 … x).
+#A #P #P' #H1 * #x #H2 @H1 @H2
+qed.
+
(* Prod *)
record Prod (A,B:Type[0]) : Type[0] ≝ {