X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_reqx.ma;h=61b24fdae03d8bf440c33ca30ae7eb9aae45d6b7;hb=c7b50fec51b9a25d5bc536f44e54179fd53efb44;hp=b0b50cf3ac0df6f60f8d94b4d2fe09c66183a99e;hpb=adb9ba187619cea977d1d22971eba27eb437cd6a;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
index b0b50cf3a..61b24fdae 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
@@ -134,7 +134,7 @@ elim (cpx_teqx_conf_rex … HT01 … HT02 L … L) -HT01 -HT02
 qed-.
 
 lemma teqx_cpx_trans: ∀h,G,L,T2. ∀T0:term. T2 ≛ T0 →
-                      ∀T1. ⦃G,L⦄ ⊢ T0 ⬈[h] T1 → 
+                      ∀T1. ⦃G,L⦄ ⊢ T0 ⬈[h] T1 →
                       ∃∃T. ⦃G,L⦄ ⊢ T2 ⬈[h] T & T ≛ T1.
 #h #G #L #T2 #T0 #HT20 #T1 #HT01
 elim (cpx_teqx_conf … HT01 T2) -HT01 /3 width=3 by teqx_sym, ex2_intro/