milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / csx_simple.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma
index d6d1c109491a51410c7689ec5201e9c5a76d11eb..1f732d61de1301712fd21341983588b9f64ead04 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple.ma
@@ -15,22 +15,23 @@
 include "basic_2/rt_transition/cpx_simple.ma".
 include "basic_2/rt_computation/csx_csx.ma".
 
-(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********)
+(* STRONGLY NORMALIZING TERMS FOR EXTENDED PARALLEL RT-TRANSITION ***********)
 
 (* Properties with simple terms *********************************************)
 
-lemma csx_appl_simple: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1.
-                       (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) →
-                       𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄.
-#h #o #G #L #V #H @(csx_ind … H) -V
+lemma csx_appl_simple (G) (L):
+      ∀V. ❪G,L❫ ⊢ ⬈*𝐒 V → ∀T1.
+      (∀T2. ❪G,L❫ ⊢ T1 ⬈ T2 → (T1 ≛ T2 → ⊥) → ❪G,L❫ ⊢ ⬈*𝐒 ⓐV.T2) →
+      𝐒❪T1❫ → ❪G,L❫ ⊢ ⬈*𝐒 ⓐV.T1.
+#G #L #V #H @(csx_ind … H) -V
 #V #_ #IHV #T1 #IHT1 #HT1
 @csx_intro #X #H1 #H2
 elim (cpx_inv_appl1_simple … H1) // -H1
 #V0 #T0 #HLV0 #HLT10 #H destruct
-elim (tdneq_inv_pair … H2) -H2
+elim (tneqx_inv_pair … H2) -H2
 [ #H elim H -H //
 | #HV0 @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
-  @(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *) 
+  @(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *)
 | -IHV -HT1 /4 width=3 by csx_cpx_trans, cpx_pair_sn/
 ]
 qed.