X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_drops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_drops.ma;h=eaf81190d77217ce6bc0422952c171a73de348b1;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=ea4d621145b37619153dbd87489c1078b78798e1;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma index ea4d62114..eaf81190d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma @@ -33,6 +33,6 @@ lemma rpx_inv_lifts_dx (h) (G): f_dropable_dx (cpx h G). lemma rpx_inv_lifts_bi (h) (G): ∀L1,L2,U. ⦃G,L1⦄ ⊢ ⬈[h,U] L2 → ∀b,f. 𝐔⦃f⦄ → - ∀K1,K2. ⬇*[b,f] L1 ≘ K1 → ⬇*[b,f] L2 ≘ K2 → - ∀T. ⬆*[f]T ≘ U → ⦃G,K1⦄ ⊢ ⬈[h,T] K2. + ∀K1,K2. ⇩*[b,f] L1 ≘ K1 → ⇩*[b,f] L2 ≘ K2 → + ∀T. ⇧*[f]T ≘ U → ⦃G,K1⦄ ⊢ ⬈[h,T] K2. /2 width=10 by rex_inv_lifts_bi/ qed-.