A -> B -> A
intro a.
intro b.
assumption.