]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma
- dependences on ceq and ceq_ext fixed
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / syntax / tdeq_ext.ma
index 7cfeee246eead25381c8e18722462693c0dba6aa..93a3be18d31c3edc803e4a17429ad650e249b30b 100644 (file)
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/stareq_5.ma".
+include "basic_2/syntax/cext2.ma".
 include "basic_2/syntax/tdeq.ma".
-include "basic_2/syntax/lenv_ext2.ma".
 
 (* EXTENDED DEGREE-BASED EQUIVALENCE ****************************************)