- new extendedd beta-reductum involving native type annotation

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lsubr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
index eee557904ae5874c3be6e240af3e918011356749..c782c471fe2382447ce291a455dd89a7f06a8117 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma
@@ -24,10 +24,7 @@ inductive lsubr: relation lenv ≝
 
 interpretation
   "local environment refinement (substitution)"
-  'SubEq L1 L2 = (lsubr L1 L2).
-
-definition lsubr_trans: ∀S. predicate (lenv → relation S) ≝ λS,R.
-                        ∀L2,s1,s2. R L2 s1 s2 → ∀L1. L1 ⊑ L2 → R L1 s1 s2.
+  'CrSubEq L1 L2 = (lsubr L1 L2).
 
 (* Basic properties *********************************************************)
 
@@ -41,14 +38,6 @@ lemma lsubr_refl: ∀L. L ⊑ L.
 #L elim L -L // /2 width=1/
 qed.
 
-lemma TC_lsubr_trans: ∀S,R. lsubr_trans S R → lsubr_trans S (LTC … R).
-#S #R #HR #L1 #s1 #s2 #H elim H -s2
-[ /3 width=3/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #HL12
-  lapply (HR … Hs2 … HL12) -HR -Hs2 /3 width=3/
-]
-qed.
-
 (* Basic inversion lemmas ***************************************************)
 
 fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.