apply Iff.intro <;> intros h₁
case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
case impl.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹⊃a✝
⊢ a✝¹⊃a✝ ∈ ↑t

case impl.mpr
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ↑t
⊢ t⊨a✝¹⊃a✝