+nlemma Ex_morphism : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#S; @(λP: S ⇒_1 CProp[0].Ex S P); #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
+
+unification hint 0 ≔ S : setoid, P : S ⇒_1 CProp[0];
+ A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
+ B ≟ CPROP,
+ M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S P)
+ (prop11 ?? (Ex_morphism S))
+(*------------------------*)⊢
+ fun11 A B M P ≡ Ex S (fun11 S CPROP P).
+
+nlemma Ex_morphism_eta : ∀S:setoid.(S ⇒_1 CProp[0]) ⇒_1 CProp[0].
+#S; @(λP: S ⇒_1 CProp[0].Ex S (λx.P x)); #P Q E; @; *; #x Px; @x; ncases (E x x #); /2/; nqed.
+
+unification hint 0 ≔ S : setoid, P : S ⇒_1 CProp[0];
+ A ≟ unary_morphism1_setoid1 (setoid1_of_setoid S) CPROP,
+ B ≟ CPROP,
+ M ≟ mk_unary_morphism1 ?? (λP: S ⇒_1 CProp[0].Ex S (λx.P x))
+ (prop11 ?? (Ex_morphism_eta S))
+(*------------------------*)⊢
+ fun11 A B M P ≡ Ex S (λx.fun11 S CPROP P x).
+
+nlemma Ex_setoid : ∀S:setoid.(S ⇒_1 CPROP) → setoid.
+#T P; @ (Ex T (λx:T.P x)); @; ##[ #H1 H2; napply True |##*: //; ##] nqed.
+
+unification hint 0 ≔ T,P ;
+ S ≟ (Ex_setoid T P)
+(*---------------------------*) ⊢
+ Ex T (λx:T.P x) ≡ carr S.
+
+(* couts how many Ex we are traversing *)
+ninductive counter : Type[0] ≝
+ | End : counter
+ | Next : (bool → bool) → (* dummy arg please the notation mechanism *)
+ counter → counter.
+
+(* to rewrite terms (live in setoid) *)
+nlet rec mk_P (S, T : setoid) (n : counter) on n ≝
+ match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P S T m) ].
+
+nlet rec mk_F (S, T : setoid) (n : counter) on n ≝
+ match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F S T m) ].
+
+nlet rec mk_E (S, T : setoid) (n : counter) on n : ∀f,g : mk_F S T n. CProp[0] ≝
+ match n with
+ [ End ⇒ λf,g:T. f = g
+ | Next q m ⇒ λf,g: mk_F S T (Next q m). ∀x:S.mk_E S T m (f x) (g x) ].
+
+nlet rec mk_H (S, T : setoid) (n : counter) on n :
+∀P1,P2: mk_P S T n.∀f,g : mk_F S T n. CProp[1] ≝
+ match n with
+ [ End ⇒ λP1,P2:mk_P S T End.λf,g:T. f = g → P1 f =_1 P2 g
+ | Next q m ⇒ λP1,P2: mk_P S T (Next q m).λf,g: mk_F S T (Next q m).
+ ∀x:S.mk_H S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex (S, T : setoid) (n : counter) on n :
+∀P: mk_P S T n.∀f : mk_F S T n. CProp[0] ≝
+ match n with
+ [ End ⇒ λP:mk_P S T End.λf:T. P f
+ | Next q m ⇒ λP: mk_P S T (Next q m).λf: mk_F S T (Next q m).
+ ∃x:S.mk_Ex S T m (P x) (f x) ].
+
+nlemma Sig_generic : ∀S,T.∀n:counter.∀P,f,g.
+ mk_E S T n f g → mk_H S T n P P f g → mk_Ex S T n P f =_1 mk_Ex S T n P g.
+#S T n; nelim n; nnormalize;
+##[ #P f g E H; /2/;
+##| #q m IH P f g E H; @; *; #x Px; @x; ncases (IH … (E x) (H x)); /3/; ##]
+nqed.