(A \/ (B \/ C) -> (A \/ B) \/ C) /\ ((A \/ B) \/ C -> A \/ (B \/ C))
split.
intro ou.
elim ou.
intro a.
left.
left.
assumption.
intro bc.
elim bc.
intro b.
left.
right.
assumption.
intro c.
right.
assumption.
intro ou.
elim ou.
intro ab.
elim ab.
intro a.
left.
assumption.
intro b.
right.
left.
assumption.
intro c.
right.
right.
assumption.