all_goals apply Iff.intro <;> intros h₁
case atom
t : Th
a✝ : ℕ
⊢ t⊨#a✝ ↔ #a✝ ∈ ↑t

case neg
t : Th
a✝ : Form
⊢ t⊨~a✝ ↔ ~a✝ ∈ ↑t

case and
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹&a✝ ↔ a✝¹&a✝ ∈ ↑t

case or
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹¦a✝ ↔ a✝¹¦a✝ ∈ ↑t

case impl
t : Th
a✝¹ a✝ : Form
⊢ t⊨a✝¹⊃a✝ ↔ a✝¹⊃a✝ ∈ ↑t
case atom.mp
t : Th
a✝ : ℕ
h₁ : t⊨#a✝
⊢ #a✝ ∈ ↑t

case atom.mpr
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ↑t
⊢ t⊨#a✝

case neg.mp
t : Th
a✝ : Form
h₁ : t⊨~a✝
⊢ ~a✝ ∈ ↑t

case neg.mpr
t : Th
a✝ : Form
h₁ : ~a✝ ∈ ↑t
⊢ t⊨~a✝

case and.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹&a✝
⊢ a✝¹&a✝ ∈ ↑t

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

case or.mp
t : Th
a✝¹ a✝ : Form
h₁ : t⊨a✝¹¦a✝
⊢ a✝¹¦a✝ ∈ ↑t

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

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✝