From: Ferruccio Guidi Date: Mon, 20 Jun 2016 21:39:29 +0000 (+0000) Subject: updating the dropable-related definitions with coafter ... X-Git-Tag: make_still_working~561 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d99a19985ae7ca20845d0a875e32f23ba06e536;p=helm.git updating the dropable-related definitions with coafter ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index e2f077575..0e6fcc72c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/relocation/rtmap_coafter.ma". include "basic_2/notation/relations/rdropstar_3.ma". include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/relocation/lreq.ma". @@ -53,18 +54,18 @@ definition d_deliftable2_sn: predicate (lenv → relation term) ≝ definition dropable_sn: predicate (rtmap → relation lenv) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f2,L2. R f2 L1 L2 → - ∀f1. f ⊚ f1 ≡ f2 → + ∀f1. f ~⊚ f1 ≡ f2 → ∃∃K2. R f1 K1 K2 & ⬇*[b, f] L2 ≡ K2. definition dropable_dx: predicate (rtmap → relation lenv) ≝ λR. ∀f2,L1,L2. R f2 L1 L2 → ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → - ∀f1. f ⊚ f1 ≡ f2 → + ∀f1. f ~⊚ f1 ≡ f2 → ∃∃K1. ⬇*[b, f] L1 ≡ K1 & R f1 K1 K2. definition dedropable_sn: predicate (rtmap → relation lenv) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f1,K2. R f1 K1 K2 → - ∀f2. f ⊚ f1 ≡ f2 → + ∀f2. f ~⊚ f1 ≡ f2 → ∃∃L2. R f2 L1 L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma index 14cce04db..8070c5716 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma @@ -24,11 +24,11 @@ lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_ #RN #RP #HN #HP #b #f #L1 #K1 #H elim H -f -L1 -K1 [ #f #Hf #X #f2 #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X /4 width=3 by lexs_atom, drops_atom, ex2_intro/ -| #f #I #L1 #K1 #V1 #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] - #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H +| #f #I #L1 #K1 #V1 #_ #IH #X #f2 #H #f1 #Hf2 elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] + #g2 #Hg2 #H2 destruct elim (lexs_inv_push1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 /3 width=3 by drops_drop, ex2_intro/ -| #f #I #L1 #K1 #V1 #W1 #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] +| #f #I #L1 #K1 #V1 #W1 #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (coafter_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 @@ -44,11 +44,11 @@ lemma lexs_liftable_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. [ #f #Hf #X #f1 #H #f2 #Hf2 >(lexs_inv_atom1 … H) -X /4 width=4 by drops_atom, lexs_atom, ex3_intro/ | #f #I #L1 #K1 #V1 #_ #IHLK1 #K2 #f1 #HK12 #f2 #Hf2 - elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct + elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct elim (IHLK1 … HK12 … Hg2) -K1 - /3 width=6 by drops_drop, lexs_next, ex3_intro/ + /3 width=6 by drops_drop, lexs_next, lexs_push, ex3_intro/ | #f #I #L1 #K1 #V1 #W1 #HLK1 #HWV1 #IHLK1 #X #f1 #H #f2 #Hf2 - elim (after_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + elim (coafter_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H #K2 #W2 #HK12 #HW12 #H destruct [ elim (H2RP … HW12 … HLK1 … HWV1) | elim (H2RN … HW12 … HLK1 … HWV1) ] -W1 elim (IHLK1 … HK12 … Hg2) -K1 @@ -57,18 +57,18 @@ lemma lexs_liftable_dedropable: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. qed-. fact lexs_dropable_aux: ∀RN,RP,b,f,L2,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → - ∀f2,L1. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ⊚ f1 ≡ f2 → + ∀f2,L1. L1 ⦻*[RN, RP, f2] L2 → ∀f1. f ~⊚ f1 ≡ f2 → ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[RN, RP, f1] K2. #RN #RP #b #f #L2 #K2 #H elim H -f -L2 -K2 [ #f #Hf #_ #f2 #X #H #f1 #Hf2 lapply (lexs_inv_atom2 … H) -H #H destruct /4 width=3 by lexs_atom, drops_atom, ex2_intro/ | #f #I #L2 #K2 #V2 #_ #IH #Hf #f2 #X #HX #f1 #Hf2 - elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct - elim (lexs_inv_next2 … HX) -HX #L1 #V1 #HL12 #HV12 #H destruct + elim (coafter_inv_nxx … Hf2) -Hf2 [2,3: // ] #g2 #Hg2 #H destruct + elim (lexs_inv_push2 … HX) -HX #L1 #V1 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -L2 -V2 -g2 /3 width=3 by drops_drop, isuni_inv_next, ex2_intro/ | #f #I #L2 #K2 #V2 #W2 #_ #HWV2 #IH #Hf #f2 #X #HX #f1 #Hf2 - elim (after_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct + elim (coafter_inv_pxx … Hf2) -Hf2 [1,3: * |*: // ] #g1 #g2 #Hg2 #H1 #H2 destruct [ elim (lexs_inv_push2 … HX) | elim (lexs_inv_next2 … HX) ] -HX #L1 #V1 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -L2 -g2 /2 width=3 by isuni_fwd_push/ #K1 #HLK1 #HK12 lapply (isuni_inv_push … Hf ??) -Hf [3,6: |*: // ] #Hf @@ -86,7 +86,7 @@ lemma lexs_dropable: ∀RN,RP. dropable_dx (lexs RN RP). lemma lexs_drops_conf_next: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀b,f,I,K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 → - ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K2,V2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2. #RN #RP #HRN #HRP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #f1 #Hf2 elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP @@ -97,7 +97,7 @@ qed-. lemma lexs_drops_conf_push: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → ∀f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀b,f,I,K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 → - ∀f1. f ⊚ ↑f1 ≡ f2 → + ∀f1. f ~⊚ ↑f1 ≡ f2 → ∃∃K2,V2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2. #RN #RP #HRN #HRP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #f1 #Hf2 elim (lexs_deliftable_dropable … HRN HRP … HLK1 … HL12 … Hf2) -L1 -f2 -HRN -HRP @@ -108,7 +108,7 @@ qed-. (* Basic_2A1: includes: lpx_sn_drop_trans *) lemma lexs_drops_trans_next: ∀RN,RP,f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀b,f,I,K2,V2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V2 → 𝐔⦃f⦄ → - ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RN K1 V1 V2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf #f1 #Hf2 elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf @@ -118,7 +118,7 @@ qed-. lemma lexs_drops_trans_push: ∀RN,RP,f2,L1,L2. L1 ⦻*[RN, RP, f2] L2 → ∀b,f,I,K2,V2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V2 → 𝐔⦃f⦄ → - ∀f1. f ⊚ ↑f1 ≡ f2 → + ∀f1. f ~⊚ ↑f1 ≡ f2 → ∃∃K1,V1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[RN, RP, f1] K2 & RP K1 V1 V2. #RN #RP #f2 #L1 #L2 #HL12 #b #f #I #K1 #V1 #HLK1 #Hf #f1 #Hf2 elim (lexs_dropable … HL12 … HLK1 … Hf … Hf2) -L2 -f2 -Hf @@ -130,7 +130,7 @@ lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref d_liftable2 RN → d_liftable2 RP → ∀f1,K1,K2. K1 ⦻*[RN, RP, f1] K2 → ∀b,f,I,L1,V1. ⬇*[b,f] L1.ⓑ{I}V1 ≡ K1 → - ∀f2. f ⊚ f1 ≡ ⫯f2 → + ∀f2. f ~⊚ f1 ≡ ⫯f2 → ∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RN L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2 elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP @@ -142,7 +142,7 @@ lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref d_liftable2 RN → d_liftable2 RP → ∀f1,K1,K2. K1 ⦻*[RN, RP, f1] K2 → ∀b,f,I,L1,V1. ⬇*[b,f] L1.ⓑ{I}V1 ≡ K1 → - ∀f2. f ⊚ f1 ≡ ↑f2 → + ∀f2. f ~⊚ f1 ≡ ↑f2 → ∃∃L2,V2. ⬇*[b,f] L2.ⓑ{I}V2 ≡ K2 & L1 ⦻*[RN, RP, f2] L2 & RP L1 V1 V2 & L1.ⓑ{I}V1≡[f]L2.ⓑ{I}V2. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I #L1 #V1 #HLK1 #f2 #Hf2 elim (lexs_liftable_dedropable … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index 2ce496bd5..485200949 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -30,7 +30,7 @@ lemma lreq_dropable: ∀RN,RP. dropable_dx (lexs RN RP). (* Basic_2A1: includes: lreq_drop_trans_be *) lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 → ∀b,f,I,K2,V. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V → 𝐔⦃f⦄ → - ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V & K1 ≡[f1] K2. #f2 #L1 #L2 #HL12 #b #f #I #K1 #V #HLK1 #Hf #f1 #Hf2 elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -f2 -L2 -Hf @@ -40,7 +40,7 @@ qed-. (* Basic_2A1: includes: lreq_drop_conf_be *) lemma lreq_drops_conf_next: ∀f2,L1,L2. L1 ≡[f2] L2 → ∀b,f,I,K1,V. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V → 𝐔⦃f⦄ → - ∀f1. f ⊚ ⫯f1 ≡ f2 → + ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K2. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V & K1 ≡[f1] K2. #f2 #L1 #L2 #HL12 #b #f #I #K1 #V #HLK1 #Hf #f1 #Hf2 elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -f2 -L1 -Hf @@ -49,7 +49,7 @@ qed-. lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 → ∀b,f,I,L1,V. ⬇*[b,f] L1.ⓑ{I}V ≡ K1 → - ∀f2. f ⊚ f1 ≡ ⫯f2 → + ∀f2. f ~⊚ f1 ≡ ⫯f2 → ∃∃L2. ⬇*[b,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V≡[f]L2.ⓑ{I}V. #f1 #K1 #K2 #HK12 #b #f #I #L1 #V #HLK1 #f2 #Hf2 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index 681e07d8c..47b1eec39 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_coafter.ma". include "basic_2/relocation/drops_drops.ma". include "basic_2/static/frees.ma". diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma index 7992f334e..e7ea1927d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma @@ -14,7 +14,7 @@ include "ground_2/notation/relations/rcoafter_3.ma". include "ground_2/relocation/rtmap_sor.ma". -include "ground_2/relocation/rtmap_istot.ma". +include "ground_2/relocation/rtmap_after.ma". (* RELOCATION MAP ***********************************************************) @@ -213,56 +213,6 @@ lemma coafter_eq_repl_fwd0: ∀f2,f1. eq_repl_fwd (λf. f2 ~⊚ f1 ≡ f). #f2 #f1 @eq_repl_sym /2 width=3 by coafter_eq_repl_back0/ qed-. -(* Main properties **********************************************************) -(* -corec theorem coafter_trans1: ∀f0,f3,f4. f0 ~⊚ f3 ≡ f4 → - ∀f1,f2. f1 ~⊚ f2 ≡ f0 → - ∀f. f2 ~⊚ f3 ≡ f → f1 ~⊚ f ≡ f4. -#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4 -[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg - cases (coafter_inv_xxp … Hg0 … H0) -g0 - #f1 #f2 #Hf0 #H1 #H2 - cases (coafter_inv_ppx … Hg … H2 H3) -g2 -g3 - #f #Hf #H /3 width=7 by coafter_refl/ -| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg - cases (coafter_inv_xxp … Hg0 … H0) -g0 - #f1 #f2 #Hf0 #H1 #H2 - cases (coafter_inv_pnx … Hg … H2 H3) -g2 -g3 - #f #Hf #H /3 width=7 by coafter_push/ -| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg - cases (coafter_inv_xxn … Hg0 … H0) -g0 * - [ #f1 #f2 #Hf0 #H1 #H2 - cases (coafter_inv_nxx … Hg … H2) -g2 - #f #Hf #H /3 width=7 by coafter_push/ - | #f1 #Hf0 #H1 /3 width=6 by coafter_next/ - ] -] -qed-. - -corec theorem coafter_trans2: ∀f1,f0,f4. f1 ~⊚ f0 ≡ f4 → - ∀f2, f3. f2 ~⊚ f3 ≡ f0 → - ∀f. f1 ~⊚ f2 ≡ f → f ~⊚ f3 ≡ f4. -#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4 -[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg - cases (coafter_inv_xxp … Hg0 … H0) -g0 - #f2 #f3 #Hf0 #H2 #H3 - cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2 - #f #Hf #H /3 width=7 by coafter_refl/ -| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg - cases (coafter_inv_xxn … Hg0 … H0) -g0 * - [ #f2 #f3 #Hf0 #H2 #H3 - cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2 - #f #Hf #H /3 width=7 by coafter_push/ - | #f2 #Hf0 #H2 - cases (coafter_inv_pnx … Hg … H1 H2) -g1 -g2 - #f #Hf #H /3 width=6 by coafter_next/ - ] -| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg - cases (coafter_inv_nxx … Hg … H1) -g1 - #f #Hg #H /3 width=6 by coafter_next/ -] -qed-. -*) (* Main inversion lemmas ****************************************************) corec theorem coafter_mono: ∀f1,f2,x,y. f1 ~⊚ f2 ≡ x → f1 ~⊚ f2 ≡ y → x ≗ y. @@ -726,3 +676,54 @@ lemma coafter_sor: ∀f. 𝐅⦃f⦄ → ∀f2. 𝐓⦃f2⦄ → ∀f1. f2 ~⊚ /3 width=11 by coafter_refl, coafter_push, sor_np, sor_pn, sor_nn, ex3_2_intro/ ] qed-. + +(* Properties with after ****************************************************) +(* +corec theorem coafter_trans1: ∀f0,f3,f4. f0 ~⊚ f3 ≡ f4 → + ∀f1,f2. f1 ~⊚ f2 ≡ f0 → + ∀f. f2 ~⊚ f3 ≡ f → f1 ~⊚ f ≡ f4. +#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4 +[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg + cases (coafter_inv_xxp … Hg0 … H0) -g0 + #f1 #f2 #Hf0 #H1 #H2 + cases (coafter_inv_ppx … Hg … H2 H3) -g2 -g3 + #f #Hf #H /3 width=7 by coafter_refl/ +| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg + cases (coafter_inv_xxp … Hg0 … H0) -g0 + #f1 #f2 #Hf0 #H1 #H2 + cases (coafter_inv_pnx … Hg … H2 H3) -g2 -g3 + #f #Hf #H /3 width=7 by coafter_push/ +| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg + cases (coafter_inv_xxn … Hg0 … H0) -g0 * + [ #f1 #f2 #Hf0 #H1 #H2 + cases (coafter_inv_nxx … Hg … H2) -g2 + #f #Hf #H /3 width=7 by coafter_push/ + | #f1 #Hf0 #H1 /3 width=6 by coafter_next/ + ] +] +qed-. + +corec theorem coafter_trans2: ∀f1,f0,f4. f1 ~⊚ f0 ≡ f4 → + ∀f2, f3. f2 ~⊚ f3 ≡ f0 → + ∀f. f1 ~⊚ f2 ≡ f → f ~⊚ f3 ≡ f4. +#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4 +[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg + cases (coafter_inv_xxp … Hg0 … H0) -g0 + #f2 #f3 #Hf0 #H2 #H3 + cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=7 by coafter_refl/ +| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg + cases (coafter_inv_xxn … Hg0 … H0) -g0 * + [ #f2 #f3 #Hf0 #H2 #H3 + cases (coafter_inv_ppx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=7 by coafter_push/ + | #f2 #Hf0 #H2 + cases (coafter_inv_pnx … Hg … H1 H2) -g1 -g2 + #f #Hf #H /3 width=6 by coafter_next/ + ] +| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg + cases (coafter_inv_nxx … Hg … H1) -g1 + #f #Hg #H /3 width=6 by coafter_next/ +] +qed-. +*)