X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_cpms.ma;h=4e6732f13baeae9a27755e075b53013106739b9d;hp=bee160dd303184529906dc28fcb6b237a0f8edac;hb=076439def28e649ec384fae038ed021dadd5f75c;hpb=d2545ffd201b1aa49887313791386add78fa8603

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
index bee160dd3..4e6732f13 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma
@@ -32,7 +32,7 @@ lemma lprs_cpm_trans (h) (n) (G) (T1:term) (T2:term):
 /3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
 
 (* Basic_2A1: includes cprs_bind2 *)
-lemma cpms_bind_dx (h) (n) (G) (L):
+lemma cpms_bind_alt (h) (n) (G) (L):
       ∀V1,V2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 →
       ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ➡*[h,n] T2 →
       ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2.