proposition: Lemma and_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]. exact (conj (a_to_c a) (b_to_d b)). Qed.
imports: Classical_Prop Classical_Pred_Type