]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
unistep_aux
[helm.git] / matita / matita / contribs / lambda / paths / labeled_st_reduction.ma
index 253f2ae736fc51090214b247891d2c78005a3206..f6f93d6fb22a4bcdbed5ed039404c2527f0ef6d3 100644 (file)
@@ -12,8 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "subterms/delifting_substitution.ma".
-include "subterms/projections.ma".
+include "subterms/booleanize.ma".
 include "paths/standard_order.ma".
 
 (* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)