theorem orb_elim: \forall b1,b2:bool. \forall P:bool \to Prop.
match b1 with
[ true \Rightarrow P true
theorem orb_elim: \forall b1,b2:bool. \forall P:bool \to Prop.
match b1 with
[ true \Rightarrow P true
definition if_then_else : bool \to Prop \to Prop \to Prop \def
\lambda b:bool.\lambda P,Q:Prop.
match b with
definition if_then_else : bool \to Prop \to Prop \to Prop \def
\lambda b:bool.\lambda P,Q:Prop.
match b with