rw [inst.appLeftIdent u]
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ Model.identity∙u⊨g
α : Type
inst : Model α
f g : Form
h₁ : ∀ (x : α), x⊨f → x⊨g
u : α
h₂ : u⊨f
⊢ u⊨g