a few more lemmas for Data.Prop.

coq-community · Apr 3, 2015 · 9d7c744 · 9d7c744
1 parent 49778e3
commit 9d7c744
Showing 1 changed file with 7 additions and 0 deletions.
diff --git 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,