Goal A -> (B -> A).
apply H0.