X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpx_frees.ma;h=c786518ee0a5b9844c6f921bba8281f60e280844;hb=a78df6200d61b34a67cb1cba9edf984aae470530;hp=7e184e1a4a64cba6e7f58f9670a1dc15d6b98d90;hpb=614542345e3e9c88722fdbc32c24a14b9a6c71d1;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma index 7e184e1a4..c786518ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma @@ -131,8 +131,8 @@ lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ elim (lsubf_frees_trans … HgT2 (⫯gVT2) … (L2.ⓓⓝW2.V2)) - [2: /4 width=3 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sle_inv_tl_sn/ ] -HgT2 - #gT0 #HgT0 #HgT20 + [2: /4 width=4 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sor_inv_sle_sn, sle_inv_tl_sn/ ] + -HgT2 #gT0 #HgT0 #HgT20 elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ @(ex2_intro … g2) @@ -159,8 +159,8 @@ lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ lapply (sor_trans2 … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 - lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) [4: |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 #HgV - lapply (sor_sym … Hg) -Hg #Hg + lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) + [4: lapply (sor_sym … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *) /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ ] ]