- exclusion binder in local environments:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / tdeq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
index 9cf106377078485474223c9cda0f4649c672418b..43f538794df2fb16772bdf15fecebe5f68c1ad2f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
@@ -26,7 +26,7 @@ inductive tdeq (h) (o): relation term ≝
 .
 
 interpretation
-   "degree-based equivalence (terms)"
+   "context-free degree-based equivalence (term)"
    'LazyEq h o T1 T2 = (tdeq h o T1 T2).
 
 (* Basic inversion lemmas ***************************************************)