X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_simple_theq.ma;h=bb3b10b0193c9fbd33e3110903a3dcc72a39e83c;hp=478f6fa0584c54a370b2493e6252707b0707a8d1;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma
index 478f6fa05..bb3b10b01 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma
@@ -24,9 +24,9 @@ include "basic_2/rt_computation/csx_csx.ma".
 
 (* Basic_1: was just: sn3_appl_appl *)
 (* Basic_2A1: was: csx_appl_simple_tsts *)
-lemma csx_appl_simple_theq: ∀h,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
-                            (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
-                            𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
+lemma csx_appl_simple_theq: ∀h,G,L,V. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ → ∀T1. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T1⦄ →
+                            (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳ T2 → ⊥) → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T2⦄) →
+                            𝐒⦃T1⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⓐV.T1⦄.
 #h #G #L #V #H @(csx_ind … H) -V
 #V #_ #IHV #T1 #H @(csx_ind … H) -T1
 #T1 #H1T1 #IHT1 #H2T1 #H3T1