Set Implicit Arguments.
Theorem and_dec : forall A B C D : Prop,{ A }+{ B } -> { C }+{ D } ->{ A /\ C }+{ (B /\ C) \/ (B /\ D) \/ (A /\ D) }.
Proof.
intros A B C D AB CD.
destruct AB; destruct CD.
- left. tauto.
- right. tauto.
- right. tauto.
- right. tauto.
Qed.