- paths and left residuals: first case of the equivalence proved!

[helm.git] / matita / matita / contribs / lambda / subterms / booleanized.ma

diff --git a/matita/matita/contribs/lambda/subterms/booleanized.ma b/matita/matita/contribs/lambda/subterms/booleanized.ma
index 87b84b26bb108cf6b99132b14a78e44b2de4e97d..b3258d224544754e69bba9d770f0a332000ebeb2 100644 (file)
--- a/matita/matita/contribs/lambda/subterms/booleanized.ma
+++ b/matita/matita/contribs/lambda/subterms/booleanized.ma
@@ -12,15 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "subterms/carrier.ma".
 include "subterms/boolean.ma".
 
-(* BOOLEANIZED SUBSET (EMPTY OR FULL)  **************************************)
+(* BOOLEANIZED SUBSET (EMPTY OR FULL) ***************************************)
 
 definition booleanized: bool → subterms → subterms ≝
    λb,F. {b}⇑⇓F.
 
-interpretation "make boolean (subterms)"
+interpretation "booleanized (subterms)"
    'ProjectSame b F = (booleanized b F).
 
 notation "hvbox( { term 46 b } ⇕ break term 46 F)"