proposition: Lemma or_func (A B C D : Prop) : (A -> C) -> (B -> D) -> (A \/ B) -> (C \/ D).
proof: Proof. intros a_to_c b_to_d ab. destruct ab as [a | b]. left; exact (a_to_c a). right; exact (b_to_d b). Qed.
imports: Classical_Prop Classical_Pred_Type