[ true \Rightarrow false
| false \Rightarrow true ].
+interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
+
definition andb : bool \to bool \to bool\def
\lambda b1,b2:bool.
match b1 with
match b2 with [true \Rightarrow true | false \Rightarrow false]
| false \Rightarrow false ].
+interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y).
+
definition orb : bool \to bool \to bool\def
\lambda b1,b2:bool.
match b1 with
match b2 with [true \Rightarrow true | false \Rightarrow false]
| false \Rightarrow false ].
+interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y).
+
definition if_then_else : bool \to Prop \to Prop \to Prop \def
\lambda b:bool.\lambda P,Q:Prop.
match b with
[ true \Rightarrow P
| false \Rightarrow Q].
+
+(*CSC: missing notation for if_then_else *)