mppa_k1c/DecBoolOps.v


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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.