cases l
x : ℕ
ψ : Formula
l : List Formula
⊢ repl_in_F x ψ (dis l) = dis (List.map (repl_in_F x ψ) l)
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (dis []) = dis (List.map (repl_in_F x ψ) [])

case cons
x : ℕ
ψ head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (dis (head✝ :: tail✝)) = dis (List.map (repl_in_F x ψ) (head✝ :: tail✝))