ex77drvtns ∃x Fx, ¬ ∃x ∃y (¬ y = x ∧ (Fx ∧ Fy)) / ∃x (Fx ∧ ∀y (¬ y = x → ¬ Fy))