- confluence of context-free reduction on terms (tpr) closed!

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / substitution / ltps_drop.ma

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma
index 07b8cfdc24492da7fca8751c9f610efa9eeed38b..1f917b8521e2eade95df56359435d6e8310b23d3 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/ltps_drop.ma
@@ -112,7 +112,7 @@ lemma ltps_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
 ]
 qed.
 
-lemma ltps_trans_conf_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+lemma ltps_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
                           ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1