Annoyingly, this requires one to prove the following in the model: (∀ x : A, ■ φ x) ⊢ ■ (∀ x : A, φ x)