1) Viene de la lógica. De False se deduce cualquier cosa. En lógica clásica False->X es lógicamente válido (una tautologia), para todo X.
2) Aquí se está probando la conmutatividad del \/, no la igualdad. Por ejemplo el -> no es conmutativo (algunos conectivos lo son y otros no). El término de prueba para lasdos disyunciones no es el mismo, por eso exact no funciona en este caso.
Saludos