(A -> B) -> ~B -> ~A
intro f.
intro b.
intro a.
apply b.
apply f.
assumption.