- some corrections and additions

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
index 70bd0d615865179e8632c8332715304f38a8ebaa..a8fb526e5a6cd799074f11081ad708dd215c66bf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
@@ -15,6 +15,9 @@
 include "basic_2/notation/relations/lazyeqalt_4.ma".
 include "basic_2/substitution/lleq_lleq.ma".
 
+(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
+
+(* Note: alternative definition of lleq *)
 inductive lleqa: relation4 ynat term lenv lenv ≝
 | lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2
 | lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2