Goal A -> B -> A.
intros.
    exact H0.
Qed.