diff options
Diffstat (limited to 'theories/Init/Logic.v')
| -rw-r--r-- | theories/Init/Logic.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index b01b80630..a91fd0480 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -150,6 +150,16 @@ Proof. intros; tauto. Qed. +Lemma iff_and : forall A B : Prop, (A <-> B) -> (A -> B) /\ (B -> A). +Proof. +intros A B []; split; trivial. +Qed. + +Lemma iff_to_and : forall A B : Prop, (A <-> B) <-> (A -> B) /\ (B -> A). +Proof. +intros; tauto. +Qed. + (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes either [P] and [Q], or [~P] and [Q] *) |