∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : L.BoundedFormula α n → Prop} {φ : L.BoundedFormula α n},
  φ.IsQF →
    P ⊥ →
      (∀ (ψ : L.BoundedFormula α n), ψ.IsAtomic → P ψ) →
        (∀ {φ₁ φ₂ : L.BoundedFormula α n}, P φ₁ → P φ₂ → P (φ₁ ⊓ φ₂)) →
          (∀ {φ : L.BoundedFormula α n}, P φ → P φ.not) →
            (∀ {φ₁ φ₂ : L.BoundedFormula α n}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ