14 lines
159 B
Plaintext
14 lines
159 B
Plaintext
(A \/ B) -> (A -> C) -> (B -> D) -> (C \/ D)
|
|
intro ou.
|
|
intro i1.
|
|
intro i2.
|
|
elim ou.
|
|
intro a.
|
|
left.
|
|
apply i1.
|
|
assumption.
|
|
intro b.
|
|
right.
|
|
apply i2.
|
|
assumption.
|