∀x ¬ Fx / ¬ ∀x Fx
∀x Rax / ∀x Rx(fx)
∀x (Hx → ¬ Cx), Hs / ∀x ¬ Cx
∀x Oxx, ∀x ∀y (Oxy ∨ Oyx) / ∀x Oxb
∀x (Fx → ∀y Rxy) / ∀x (Fx → ∀y Ryx)
∀x (Fxa → Gx), ∀x Fxx / ∀x (x = d → Gx)
∀x ¬ ∀y ¬ Rxy / ⊥
∀x Rx(fx) / ⊥