Theorem: repl_in_Con (Pdl/Substitution.lean)

State before:
x : ℕ
ψ : Formula
l : List Formula
⊢ repl_in_F x ψ (Con l) = Con (List.map (repl_in_F x ψ) l)
Tactic:
cases l
State after:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (Con []) = Con (List.map (repl_in_F x ψ) [])

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

State before:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (Con []) = Con (List.map (repl_in_F x ψ) [])
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ψ φ1 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: l)) = Con (List.map (repl_in_F x ψ) (φ1 :: l))
Tactic:
cases l
State after:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (Con [φ1]) = Con (List.map (repl_in_F x ψ) [φ1])

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

State before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: φ2 :: l)) = Con (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
case cons φ2 l =>
  simp [Con]
  apply repl_in_Con
State after:
no goals

State before:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (Con [φ1]) = Con (List.map (repl_in_F x ψ) [φ1])
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: φ2 :: l)) = Con (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
simp [Con]
State after:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ2 :: l)) = Con (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)

State before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ2 :: l)) = Con (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)
Tactic:
apply repl_in_Con
State after:
no goals