[ true \Rightarrow false
| false \Rightarrow true ].
+(*CSC: the URI must disappear: there is a bug now *)
interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
definition andb : bool \to bool \to bool\def
match b2 with [true \Rightarrow true | false \Rightarrow false]
| false \Rightarrow false ].
+(*CSC: the URI must disappear: there is a bug now *)
interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y).
definition orb : bool \to bool \to bool\def
match b2 with [true \Rightarrow true | false \Rightarrow false]
| false \Rightarrow false ].
+(*CSC: the URI must disappear: there is a bug now *)
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