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