made executable again

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx_simple.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma
index 1ce5b538d7aa0a0a906caba74c59855f6d138b93..e5c330f80c34be7ce44d9327d92d07a5a8d9da31 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_simple.ma
@@ -15,13 +15,13 @@
 include "basic_2/rt_transition/cpg_simple.ma".
 include "basic_2/rt_transition/cpx.ma".
 
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS **************)
 
 (* Inversion lemmas with simple terms ***************************************)
 
-lemma cpx_inv_appl1_simple: ∀h,G,L,V1,T1,U. ⦃G,L⦄ ⊢ ⓐV1.T1 ⬈[h] U → 𝐒⦃T1⦄ →
-                            ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[h] V2 & ⦃G,L⦄ ⊢ T1 ⬈[h] T2 &
-                                     U = ⓐV2.T2.
-#h #G #L #V1 #T1 #U * #c #H #HT1 elim (cpg_inv_appl1_simple … H) -H
+lemma cpx_inv_appl1_simple (G) (L):
+      ∀V1,T1,U. ❨G,L❩ ⊢ ⓐV1.T1 ⬈ U → 𝐒❨T1❩ →
+      ∃∃V2,T2. ❨G,L❩ ⊢ V1 ⬈ V2 & ❨G,L❩ ⊢ T1 ⬈ T2 & U = ⓐV2.T2.
+#G #L #V1 #T1 #U * #c #H #HT1 elim (cpg_inv_appl1_simple … H) -H
 /3 width=5 by ex3_2_intro, ex_intro/
 qed-.