cases α
x : ℕ
α : Program
x_notin : x ∉ voc α
F : List Formula
δ : List Program
Fδ_in_H : (F, δ) ∈ H α
⊢ x ∉ voc F ∧ x ∉ voc δ
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : x ∉ voc (·a✝)
Fδ_in_H : (F, δ) ∈ H (·a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹;'a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹;'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹⋓a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹⋓a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ voc (∗a✝)
Fδ_in_H : (F, δ) ∈ H (∗a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ