33 lines
343 B
Plaintext
33 lines
343 B
Plaintext
(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.
|