apply And.intro
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f&g
case left
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨f

case right
α : Type
inst : Model α
s t : α
f✝ : Form
h₁ : s ≤ t
f g : Form
h₂ : s⊨f&g
⊢ t⊨g