apply repl_in_P_non_occ_eq
case right
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ repl_in_P x ρ γ = γ
case right.a
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ x ∉ voc γ