+lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop.
+ \forall R : (\forall x:S. P x \to Prop). \forall x : S.
+ extend S P R x \to (sigT ? (λH : P x. R x H)).
+intros.
+elim e.
+apply (existT).assumption.
+apply (t1 t).
+qed.
+
+(*
+lemma ext2_a : \forall S:CSetoid. \forall P: S \to Prop.
+ \forall R : (\forall x:S. P x \to Prop). \forall x : S.
+ extend S P R x \to (ex ? (λH : P x. R x H)).
+intros.
+elim H.
+apply (ex_intro).
+exact H1.apply H2.
+qed.
+*)
+definition proj1_sigT: \forall A : Type. \forall P : A \to Type.
+ \forall e : sigT A P. ? \def
+ \lambda A : Type. \lambda P : A \to Type.
+ \lambda e : sigT A P.
+ match e with
+ [existT a b \Rightarrow a].
+
+(* original def in CLogic.v
+Definition proj1_sigT (A : Type) (P : A -> CProp) (e : sigT P) :=
+ match e with
+ | existT a b => a
+ end.
+*)
+(* _ *)
+definition proj2_sigTm : \forall A : Type. \forall P : A \to Type.
+ \forall e : sigT A P. ? \def
+ \lambda A : Type. \lambda P : A \to Type.
+ \lambda e : sigT A P.
+ match e return \lambda s:sigT A P. P (proj1_sigT A P s) with
+ [ existT a b \Rightarrow b].
+
+definition projT1: \forall A: Type. \forall P: A \to Type.\forall H: sigT A P. A \def
+ \lambda A: Type. \lambda P: A \to Type.\lambda H: sigT A P.
+ match H with
+ [existT x b \Rightarrow x].
+
+definition projT2m : \forall A: Type. \forall P: A \to Type. \forall x:sigT A P.
+ P (projT1 A P x) \def
+ \lambda A: Type. \lambda P: A \to Type.
+ (\lambda H:sigT A P.match H return \lambda s:sigT A P. P (projT1 A P s) with
+ [existT (x:A) (h:(P x))\Rightarrow h]).
+
+lemma ext2 : \forall S:CSetoid. \forall P: S \to Prop.
+\forall R : (\forall x:S. P x \to Prop).
+\forall x: S.
+ \forall Hx:extend S P R x.
+ R x (proj1_sigT ? ? (ext2_a S P R x Hx)).
+ intros.
+ elim ext2_a.
+ apply (projT2m (P x) (\lambda Hbeta:P x.R x a)).
+ apply (existT (P x) ).assumption.assumption.
+qed.