- some renaming

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / yprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
index bb4daf0be081cb16cd1b576a2eb81835b32331e2..2bf1ae018495ab4476371e9c52ef4119c96668f0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma
@@ -72,7 +72,7 @@ qed.
 lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄.
 /3 width=1/ qed.
 
-lemma lpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ ➡ L2 → L2 ⊢ T1 ➡* T2 →
+lemma cprs_lpr_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ T1 ➡* T2 → L1 ⊢ ➡ L2 →
                      h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=4 by yprs_strap2, ypr_lpr, cprs_yprs/
+/3 width=4 by yprs_strap1, ypr_lpr, cprs_yprs/
 qed.