Goal A -> B -> A.
intros.
    exact H3.
    apply H5.
exact H0.
Qed.