xoa notation refactoring and minor additions

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / xoa / xoa_props.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
index e917bacd22b087b846167fb63b3fabe842501653..408e1933dec9e3c55744a695c6c63f6a22e8238e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma
@@ -15,6 +15,8 @@
 include "basics/logic.ma".
 include "ground_2/notation/xoa/false_0.ma".
 include "ground_2/notation/xoa/true_0.ma".
+include "ground_2/notation/xoa/or_2.ma".
+include "ground_2/notation/xoa/and_2.ma".
 include "ground_2/xoa/xoa.ma".
 
 interpretation "logical false" 'false = False.