all_goals
  simp [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram] at *
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 δ
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : ¬x = a✝
Fδ_in_H : F = [] ∧ δ = [·a✝]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1