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