+ [ true \Rightarrow true
+ | false \Rightarrow b2].
+
+theorem orb_elim: \forall b1,b2:bool. \forall P:bool \to Prop.
+match b1 with
+[ true \Rightarrow P true
+| false \Rightarrow P b2] \to P (orb b1 b2).
+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).