+ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
+#S; @; ##[ #P; napply (Ex ? P); ##| #P1 P2 E; @;
+*; #x; #H; @ x; nlapply (E x x ?); //; *; /2/;
+nqed.
+
+nlemma d : ∀S:Alpha.
+ ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
+ ∀x,y:list S.x = y →
+ let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
+ form x = form y.
+ #S ee x y E;
+ nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
+
+ nnormalize;
+ nlapply (exists_is_morph (list S) (list S) ? ?? E);
+
+ nchange with (F x = F y);
+ nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+ napply (.= † E);
+ napply #.
+nqed.
+
+
+E : w = w2
+
+
+ Σ(λx.(#‡E)‡#) : ∃x.x = w ∧ m → ∃x.x = w2 ∧ m
+ λx.(#‡E)‡# : ∀x.x = w ∧ m → x = w2 ∧ m
+
+
+w;
+F ≟ ex_moprh ∘ G
+g ≟ fun11 G
+------------------------------
+ex (λx.g w x) ==?== fun11 F w
+
+x ⊢ fun11 ?h ≟ λw. ?g w x
+?G ≟ morphism_leibniz (T → S) ∘ ?h
+------------------------------
+(λw. (λx:T.?g w x)) ==?== fun11 ?G
+
+...
+x ⊢ fun11 ?h ==?== λw. eq x w ∧ m [w]
+(λw,x.eq x w ∧ m[w]) ==?== fun11 ?G
+ex (λx.?g w x) ==?== ex (λx.x = w ∧ m[w])
+
+ndefinition ex_morph : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
+#S; @; ##[ #P; napply (Ex ? P); ##| ncases admit. ##] nqed.
+
+ndefinition ex_morph1 : ∀S:setoid. (S ⇒_1 CPROP) ⇒_1 CPROP.
+#S; @; ##[ #P; napply (Ex ? (λx.P); ##| ncases admit. ##] nqed.
+
+
+nlemma d : ∀S:Alpha.
+ ∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.
+ ∀x,y:list S.x = y →
+ let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
+ form x = form y.
+ #S ee x y E;
+ nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
+
+ nnormalize;
+
+ nchange with (F x = F y);
+ nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+ napply (.= † E);
+ napply #.
+nqed.
+
+
+nlemma d : ∀S:Alpha.∀ee: (setoid1_of_setoid (list S)) ⇒_1 (setoid1_of_setoid (list S)) ⇒_1 CPROP.∀x,y:list S.x = y →
+ let form ≝ comp1_unary_morphisms ??? (ex_morph (list S)) ee in
+ form x = form y.
+ #S ee x y E;
+ nletin F ≝ (comp1_unary_morphisms ??? (ex_morph (list S)) ee);
+
+ nnormalize;
+
+ nchange with (F x = F y);
+ nchange in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+ napply (.= † E);
+ napply #.
+nqed.
+
+
+nlemma d : ∀S:Alpha.(setoid1_of_setoid (list S)) ⇒_1 CPROP.
+ #S; napply (comp1_unary_morphisms ??? (ex_morph (list S)) ?);
+ napply (eq1).
+
+
+
+(*
+ndefinition comp_ex : ∀X,S,T,K.∀P:X ⇒_1 (S ⇒_1 T).∀Pc : (S ⇒_1 T) ⇒_1 K. X ⇒_1 K.
+ *)
+
+ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
+#S r; @(𝐋\p r); #w1 w2 E; nelim r; /2/;
+##[ #x; @; #H; ##[ nchange in H ⊢ % with ([?]=?); napply ((.= H) E)]
+ nchange in H ⊢ % with ([?]=?); napply ((.= H) E^-1);
+##| #e1 e2 H1 H2;
+ nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+ napply (.= (#‡H2));
+ napply (.= (Eexists ?? ? w1 w2 E)‡#);
+
+
+ nchange in match (w2 ∈ 𝐋\p (?·?)) with (?∨?);
+ napply (.=
+
+
+ //; napply (trans ?? ??? H E);
+ napply (trans (list S) (eq0 (LIST S)) ? [?] ?(*w1 [x] w2*) H E);
+ nlapply (trans (list S) (eq0 (LIST S))).
+
+napply (.= H); nnormalize; nlapply (trans ? [x] w1 w2 E H); napply (.= ?) [napply (w1 = [x])] ##[##2: napply #; napply sym1; napply refl1 ]
+
+ndefinition epsilon ≝
+ λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].