From 9d7c7449778ecb8111c0765c542eb5feba4ce2c2 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Thu, 2 Apr 2015 23:49:30 -0700 Subject: [PATCH] a few more lemmas for Data.Prop. --- theories/Data/Prop.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/theories/Data/Prop.v b/theories/Data/Prop.v index 80b1fac4..1bf0093e 100644 --- a/theories/Data/Prop.v +++ b/theories/Data/Prop.v @@ -67,6 +67,13 @@ Lemma impl_iff ((P -> Q) <-> (R -> S)). Proof. clear. intuition. Qed. +Lemma impl_eq : forall (P Q : Prop), P = Q -> (P -> Q). +Proof. clear. intros; subst; auto. Qed. + +Lemma uncurry : forall (P Q R : Prop), + (P /\ Q -> R) <-> (P -> Q -> R). +Proof. clear. tauto. Qed. + (** Forall **) Lemma forall_iff : forall T P Q,