lsubs renamed as lsubr

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index e20ce0559c9639a07234ac19a1f0511533883e13..ccfa7901101fbe13f2de5f735ff41e3403ad812f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -59,7 +59,7 @@ lemma cprs_strap2: ∀L,T1,T,T2.
 /2 width=3/ qed.
 
 (* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
+lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
                         ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
 /3 width=3/
 qed.