+interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
+interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
+
+
+nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
+ ∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
+#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
+
+notation "∑" non associative with precedence 90 for @{Sig ?????}.
+
+nlemma test : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y → (Ex S (λw.ee x w ∧ True)) =_1 (Ex S (λw.ee y w ∧ True)).
+#S m x y E;
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #)╪_1 #))).
+napply #.
+nqed.
+
+nlemma test2 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y →
+ (True ∧ (Ex S (λw.ee x w ∧ True))) =_1 (True ∧ (Ex S (λw.ee y w ∧ True))).
+#S m x y E;
+napply (.=_1 #╪_1(∑ E (λw,H.(H ╪_1 #) ╪_1 #))).
+napply #.
+nqed.
+
+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.
+
+nlemma test3 : ∀S:setoid. ∀ee: S ⇒_1 S ⇒_1 CPROP.
+ ∀x,y:setoid1_of_setoid S.x =_1 y →
+ ((Ex S (λw.ee x w ∧ True) ∨ True)) =_1 ((Ex S (λw.ee y w ∧ True) ∨ True)).
+#S m x y E;
+napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
+napply #.
+nqed.
+
+ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
+#S r; @(𝐋\p r); #w1 w2 E; nelim r;
+##[ /2/;
+##| /2/;
+##| #x; @; *;
+##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
+ napply ((.=_0 H) E^-1);
+##| #e1 e2 H1 H2;
+ nchange in match (w1 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+ nchange in match (w2 ∈ 𝐋\p (?·?)) with ((∃_.?)∨?);
+ napply (.= (#‡H2));
+ napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))╪_1 #); ##[
+ ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+ @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+ napply ( (X‡#)‡#); ##]
+ napply #;
+##| #e1 e2 H1 H2;
+ nnormalize in ⊢ (???%%);
+ napply (H1‡H2);
+##| #e H; nnormalize in ⊢ (???%%);
+ napply (.=_1 (∑ E (λx1,H1.∑ E (λx2,H2.?)))); ##[
+ ncut ((w1 = (x1@x2)) = (w2 = (x1@x2)));##[
+ @; #X; ##[ napply ((.= H1^-1) X) | napply ((.= H2) X) ] ##] #X;
+ napply ((X‡#)‡#); ##]
+ napply #;##]
+nqed.
+
+unification hint 0 ≔ S : Alpha,e : pitem S;
+ SS ≟ (list S),
+ X ≟ (mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e)))
+(*-----------------------------------------------------------------*)⊢
+ ext_carr SS X ≡ 𝐋\p e.
+
+ndefinition epsilon ≝
+ λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ].