case sequence β γ =>
  constructor <;> (apply repl_in_P_non_occ_eq; tauto)
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ repl_in_P x ρ β = β ∧ repl_in_P x ρ γ = γ
no goals