X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfpxs_lpxs.ma;h=21beea53bf176b66b4e92bef5f43cc3f44be5d06;hb=268e7f336d036f77ffc9663358e9afda92b97730;hp=746bc369e0b5c13727b950567702a7a71f94b004;hpb=e8971d3db8935436e6dddc27fe1ae168c7f3b315;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
index 746bc369e..21beea53b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma
@@ -26,11 +26,11 @@ lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢
 /2 width=1 by tc_lfxs_lex/ qed.
 
 lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L →
-                       ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
+                       ∀L2,T. L ≐[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2.
 /2 width=3 by tc_lfxs_lex_lfeq/ qed.
 
 (* Inversion lemmas with uncounted parallel rt-computation for local envs ***)
 
 lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
-                           ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
-/3 width=5 by lfpx_fsle_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.
+                           ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≐[T] L2.
+/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.