]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
- degree-based equivalene for terms
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / s_transition / fqu.ma
index 043d01598be81263c10ff5b8ff8e8e99e3f193e0..f5ef91e0cf714e9e755b0afe05aa6a4fe5fc47b7 100644 (file)
@@ -13,8 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/supterm_6.ma".
-include "basic_2/grammar/lenv.ma".
-include "basic_2/grammar/genv.ma".
+include "basic_2/syntax/lenv.ma".
+include "basic_2/syntax/genv.ma".
 include "basic_2/relocation/lifts.ma".
 
 (* SUPCLOSURE ***************************************************************)