proposition: Theorem or_assoc : forall P Q R : Prop, P \/ (Q \/ R) <-> (P \/ Q) \/ R.
proof: Proof. intros P Q R. split. - intros [H | [H | H]]. + left. left. apply H. + left. right. apply H. + right. apply H. - intros [[H | H] | H]. + left. apply H. + right. left. apply H. + right. right. apply H. Qed.