Goal A -> B -> A.
intros.
try intro.
Undo.
intro.
exact H0.
Qed.