definition cdeq: ∀h. sd h → relation3 lenv term term ≝
λh,o,L. tdeq h o.
+definition tdeq_ext: ∀h. sd h → relation bind ≝
+ λh,o. ext2 (tdeq h o).
+
definition cdeq_ext: ∀h. sd h → relation3 lenv bind bind ≝
λh,o. cext2 (cdeq h o).
interpretation
- "degree-based equivalence (binders)"
- 'LazyEq h o I1 I2 = (ext2 (tdeq h o) I1 I2).
+ "degree-based equivalence (binder)"
+ 'LazyEq h o I1 I2 = (tdeq_ext h o I1 I2).