all_goals
  constructor <;> intro y y_in
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 sequence.left
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
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case sequence.right
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
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

case union.left
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✝
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case union.right
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✝
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

case star.left
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
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case star.right
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
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y