diff options
| -rw-r--r-- | theories/Init/Logic.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index e1bb443a6..4fca1d1db 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -112,6 +112,16 @@ Proof. intros; tauto. Qed. +Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A. +Proof. +intros; tauto. +Qed. + +Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C. +Proof. +intros; tauto. +Qed. + Theorem or_cancel_l : forall A B C : Prop, (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)). Proof. @@ -124,6 +134,16 @@ Proof. intros; tauto. Qed. +Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A). +Proof. +intros; tauto. +Qed. + +Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C. +Proof. +intros; tauto. +Qed. + (** Backward direction of the equivalences above does not need assumptions *) Theorem and_iff_compat_l : forall A B C : Prop, |