+unification hint 0 ≔ T : setoid,P ;
+ S ≟ (Ex_setoid T P)
+(*---------------------------*) ⊢
+ Ex (carr T) (λx:carr T.fun11 ?? P x) ≡ carr S.
+
+(* couts how many Ex we are traversing *)
+ninductive counter : Type[0] ≝
+ | End : counter
+ | Next : (Prop → Prop) → (* 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.
+
+(* to rewrite propositions (live in setoid1) *)
+nlet rec mk_P1 (S : setoid) (T : setoid1) (n : counter) on n ≝
+ match n with [ End ⇒ T → CProp[0] | Next _ m ⇒ S → (mk_P1 S T m) ].
+
+nlet rec mk_F1 (S : setoid) (T : setoid1) (n : counter) on n ≝
+ match n with [ End ⇒ T | Next _ m ⇒ S → (mk_F1 S T m) ].
+
+nlet rec mk_E1 (S : setoid) (T : setoid1) (n : counter) on n : ∀f,g : mk_F1 S T n. CProp[1] ≝
+ match n with
+ [ End ⇒ λf,g:T. f =_1 g
+ | Next q m ⇒ λf,g: mk_F1 S T (Next q m). ∀x:S.mk_E1 S T m (f x) (g x) ].
+
+nlet rec mk_H1 (S : setoid) (T : setoid1) (n : counter) on n :
+∀P1,P2: mk_P1 S T n.∀f,g : mk_F1 S T n. CProp[1] ≝
+ match n with
+ [ End ⇒ λP1,P2:mk_P1 S T End.λf,g:T. f = g → P1 f =_1 P2 g
+ | Next q m ⇒ λP1,P2: mk_P1 S T (Next q m).λf,g: mk_F1 S T (Next q m).
+ ∀x:S.mk_H1 S T m (P1 x) (P2 x) (f x) (g x) ].
+
+nlet rec mk_Ex1 (S : setoid) (T : setoid1) (n : counter) on n :
+∀P: mk_P1 S T n.∀f : mk_F1 S T n. CProp[0] ≝
+ match n with
+ [ End ⇒ λP:mk_P1 S T End.λf:T. P f
+ | Next q m ⇒ λP: mk_P1 S T (Next q m).λf: mk_F1 S T (Next q m).
+ ∃x:S.mk_Ex1 S T m (P x) (f x) ].
+
+nlemma Sig_generic1 : ∀S,T.∀n:counter.∀P,f,g.
+ mk_E1 S T n f g → mk_H1 S T n P P f g → mk_Ex1 S T n P f =_1 mk_Ex1 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/; ##]