27 lines
310 B
Plaintext
27 lines
310 B
Plaintext
( (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.
|