apply iff_intro!
case hbox
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟷ (□p✝)ⱽ
case hbox.h₁
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! □p✝ ⟶ (□p✝)ⱽ

case hbox.h₂
α : Type u_1
inst✝ : DecidableEq α
p p✝ : Formula α
a✝ : 𝐕𝐞𝐫 ⊢! p✝ ⟷ p✝ⱽ
⊢ 𝐕𝐞𝐫 ⊢! (□p✝)ⱽ ⟶ □p✝