13 lines
133 B
Plaintext
13 lines
133 B
Plaintext
(A \/ B) -> (~A -> B)
|
|
intro ou.
|
|
intro aa.
|
|
elim ou.
|
|
intro a.
|
|
cut False.
|
|
intro ff.
|
|
elim ff.
|
|
apply aa.
|
|
assumption.
|
|
intro b.
|
|
assumption.
|