-napply (trans1 ?????
-(#‡
- (Sig ????? E (λw,H.
- (prop11 ?(unary_morphism1_setoid1 ??)???
- (prop11 ?(unary_morphism1_setoid1 ??)???
- H
- ?? (refl ???))
- ?? (refl1 ???)))))).
-napply refl1.
-
-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. *)
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-
-alias symbol "trans" (instance 1) = "trans1".
-alias symbol "prop2" (instance 3) = "prop21".
-(*napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#))); *)
-
-(* OK *)
-napply (.= (Sig ? ? (?) ?? E (λw,H.
- (prop11 ?(unary_morphism1_setoid1 ??)???
- (prop11 ?(unary_morphism1_setoid1 ??)???
- H
- ?? (refl ???))
- ?? (refl1 ???))))).
-napply refl1.
-
- (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ????
- (prop11 (setoid1_of_setoid ?) (ext_powerclass_setoid ?) ? ? ????
- H
- (refl ??))
- (refl ? True))))).
-
-prop11 ???????? (prop11 ???????? H (refl ??)) (refl ??))));
-
-napply (.= (Sig ? S (λw,x. m x w ∧ True) ?? E (λw,H.(H‡#)‡#)));
-
-
-napply (.= (Sig ? S (λw,x.?) ?? E (λw,H.(H‡#)‡#)));
-(Ex S (λx.?P x y)) ==?==
-//; 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.
-
-
-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 #.