constructor <;> intro y y_in
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 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