assumption.
qed.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
+interpretation "boolean not" 'not x = (notb x).
definition andb : bool \to bool \to bool\def
\lambda b1,b2:bool.
[ true \Rightarrow b2
| 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).
+interpretation "boolean and" 'and x y = (andb x y).
theorem andb_elim: \forall b1,b2:bool. \forall P:bool \to Prop.
match b1 with
intros 3.elim b1.exact H. exact H.
qed.
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y).
+interpretation "boolean or" 'or x y = (orb x y).
definition if_then_else : bool \to Prop \to Prop \to Prop \def
\lambda b:bool.\lambda P,Q:Prop.