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