Help with Or Elimination and Bi-conditional Introduction