proposition: Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C.
proof: Proof. intros; split; [ intros [[?|?]|?]| intros [?|[?|?]]]. + left; assumption. + right; left; assumption. + right; right; assumption. + left; left; assumption. + left; right; assumption. + right; assumption. Qed.
imports: Notations Ltac