the theory of extended multiple substitution for therms is complete

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / lsuby.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
index d2aa16144f046f547edd2235e5b7019071e9e612..3c89103c3d985e955779bdfe65ac11d6b400c8c5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma
@@ -31,10 +31,6 @@ interpretation
   "local environment refinement (extended substitution)"
   'ExtLRSubEq L1 d e L2 = (lsuby d e L1 L2).
 
-definition lsuby_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
-                        ∀L2,s1,s2. R L2 s1 s2 →
-                        ∀L1,d,e. L1 ⊑×[d, e] L2 → R L1 s1 s2.
-
 (* Basic properties *********************************************************)
 
 lemma lsuby_pair_lt: ∀I1,I2,L1,L2,V,e. L1 ⊑×[0, e-1] L2 → 0 < e →
@@ -62,10 +58,6 @@ lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[0, 0] L2.
 ]
 qed.
 
-lemma TC_lsuby_trans: ∀S,R. lsuby_trans S R → lsuby_trans S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2 /3 width=7 by step, inj/
-qed.
-
 (* Basic inversion lemmas ***************************************************)
 
 fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 = ⋆.