refactoring ...

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

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
index 10102eca507257b1fa64d5e889f8aa3e100b42c9..fda5cbabd2c205b2688b78a0e6110e1730b767da 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma
@@ -84,6 +84,7 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 →
 qed.
 
 (* Note: the constant 1 comes from tps_subst *)
+(* Basic-1: was: subst1_trans *)
 theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 →
                       ∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e →
                       L ⊢ T1 [d, e] ≫ T2.