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].
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].