apply Iff.intro
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g ↔ ∀ (x : α), x⊨f → x⊨g
case mp
α : Type
inst : Model α
f g : Form
⊢ Model.identity⊨f⊃g → ∀ (x : α), x⊨f → x⊨g

case mpr
α : Type
inst : Model α
f g : Form
⊢ (∀ (x : α), x⊨f → x⊨g) → Model.identity⊨f⊃g