1 files changed, 15 insertions, 0 deletions
diff --git a/mppa_k1c/DecBoolOps.v b/mppa_k1c/DecBoolOps.v
new file mode 100644
index 00000000..7f6f7c87
--- /dev/null
+++ b/mppa_k1c/DecBoolOps.v
@@ -0,0 +1,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.
+
+  
+\ No newline at end of file