Hola Pablo.
El unfold y los intros para agregar hipótesis al contexto están bien.
el elim entiendo que es de la hipótesis con A\/~A. De aquí se generan dos obligaciones de prueba: una con hipótesis A y otra con ~A.
En el primer caso (teniendo A) para probar el or deberías tratar de probar ~B (esto es, elegir right). Al hacer unfold de ~B y luego intro la situación es que deberías probar False, pero vas a tener como hipótesis tanto A como B. Acordate que tenés la hipótesis con ~(A /\ B). Esto es: (A /\ B) -> False. Te dejo a vos el resto de la prueba en este caso.
En el segundo caso (teniendo ~A) para probar el or del goal es muy simple!
Espero que te sirva, sino volvé a escribir.
Saludos, Carlos