+| pk r1 ⇒ 𝐋\p\ r1 · 𝐋 (|r1|^* ) ].
+notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'L_pi $E}.
+notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
+interpretation "in_pl" 'L_pi E = (L_pi ? E).
+
+unification hint 0 ≔ S,a,b;
+ R ≟ LIST S
+(* -------------------------------------------- *) ⊢
+ eq_list S a b ≡ eq_rel (list S) (eq0 R) a b.
+
+notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+notation "B ⇒\sub 0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+
+interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).
+interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
+
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
+
+nlemma exists_is_morph: (* BUG *) ∀S,T:setoid.∀P: S ⇒_1 (T ⇒_1 (CProp[0]:?)).
+ ∀y,z:S.y =_0 z → (Ex T (P y)) = (Ex T (P z)).
+#S T P y z E; @;
+##[ *; #x Px; @x; alias symbol "refl" (instance 4) = "refl".
+ alias symbol "prop2" (instance 2) = "prop21".
+ napply (. E^-1‡#); napply Px;
+##| *; #x Px; @x; napply (. E‡#); napply Px;##]
+nqed.
+
+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 Sig: ∀S,T:setoid.∀P: S → (T → CProp[0]).
+ ∀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.
+
+
+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;
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "refl" (instance 5) = "refl".
+alias symbol "prop2" (instance 3) = "prop21".
+alias symbol "trans" (instance 1) = "trans1".
+alias symbol "prop2" (instance 3) = "prop21".
+(* super bug 1+1:
+ eseguire senza modificare per ottenrere degli alias, fare back di 1 passo
+ e ri-eseguire. Se riesegue senza aggiungere altri alias allora hai gli
+ alias giusti (ma se fate back di più passi, gli alias non vanno più bene...).
+ ora (m x w) e True possono essere sostituiti da ?, se invece
+ si toglie anche l'∧, allora un super bug si scatena (meta contesto locale
+ scazzato, con y al posto di x, unificata con se stessa ma col contesto
+ locale corretto...). lo stesso (o simile) bug salta fuori se esegui
+ senza gli alias giusti con ? al posto di True o (m x w).
+
+ bug a parte, pare inferisca tutto lui...
+ la E astratta nella prova è solo per fargli inferire x e y, se Sig
+ lo si riformula in modo più naturale (senza y=z) allora bisogna passare
+ x e y esplicitamente. *)
+napply (.= (Sig ? S (λw,x.(m x w) ∧ True) ?? E (λw,E.(E‡#)‡#)));
+//; nqed.
+STOP
+napply (λw:S.(.= ((E‡#)‡#)) #); ##[##2: napply w| napply m. #H; napply H;
+
+
+
+ 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 in E with (eq_rel1 ? (eq1 (setoid1_of_setoid (LIST S))) x y);
+
+ ncheck (exists_is_morph (LIST S) (LIST S) ? ?? (E‡#)).
+ nletin xxx ≝ (exists_is_morph); (LIST S)); (LIST S) ee x y 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.
+