-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 d : ∀S:setoid1. ∀ee: S ⇒_1 S ⇒_1 CPROP.
- ∀x,y:S.x =_1 y → (Ex1 S (λw.ee x w)) =_1 (Ex1 S (λw.ee y w)).
- 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.
-
-
-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.
- *)
-