reaxiomatized lleq fixes a bug in it and allows to park substitution in etc

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
index 7a9ec530ed9d9956fdf657ac017d2a7df97fe004..b431e0d1836d5e6af189f968c26bc49e235a1e6d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
@@ -25,6 +25,9 @@ interpretation
    "lazy equivalence (local environment)"
    'LazyEq T d L1 L2 = (lleq d T L1 L2).
 
+definition lleq_transitive: predicate (relation3 lenv term term) ≝
+           λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ⋕[T1, 0] L2 → R L1 T1 T2.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (