proposition: Theorem respectful_if_bool T : forall (x x' : bool) (t t' f f' : T) eqT, x = x' -> eqT t t' -> eqT f f' -> eqT (if x then t else f) (if x' then t' else f') .
proof: Proof. intros; subst; auto; destruct x'; auto. Qed.
imports: Setoid RelationClasses Morphisms