This is what is done with the following tactics Intros. I assume A and I want to prove B. But I have both A and not A.

---