Yoav Cohen (Jul 20 2026 at 19:04): Yoav Cohen (Jul 20 2026 at 19:04):
Yoav Cohen (Jul 20 2026 at 19:05):
terru (Jul 21 2026 at 11:31):Either put a - in front of your second proof (so, proof -), or end the proof one line earlier by replacing your hence with thus (what's happening is that proof without the - applies a default rule on your goal which here will be exI already, so it's been transformed to $F x \lor G x$, and your thus complains that this can't be unified with the term you gave it)
Last updated: Aug 11 2026 at 20:46 UTC