Theorem: localDiamondTruth
Proof state before:
case a
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ : List Formula × List Program
Fδ_in_Hβ : Fδ ∈ H β
⊢ (if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) =
    if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)
Tactic:
cases em (Fδ.2 = [])
Proof state after:
case a.inl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ : List Formula × List Program
Fδ_in_Hβ : Fδ ∈ H β
h✝ : Fδ.2 = []
⊢ (if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) =
    if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)

case a.inr
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
right_to_left_claim : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w ρ → evaluate M w (~⌈∗β⌉ψ)
x : ℕ := freshVarProg β
x_not_in : x ∉ voc β
σ0 : Formula :=
  dis
    (List.map
      (fun x =>
        match x with
        | (F, δ) => if δ = ε then Con F else ⊥)
      (H β))
σ1 : Formula :=
  dis
    (List.map
      (fun x_1 =>
        match x_1 with
        | (F, δ) => if δ ≠ ε then Con ((~⌈⌈δ⌉⌉~·x) :: F) else ⊥)
      (H β))
W : Type
M : KripkeModel W
w : W
this :
  repl_in_F x ρ (dis (List.map (fun Fδ => if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)) (H β))) =
    dis
      (List.map
        (fun Fδ => if Fδ.2 = [] then repl_in_F x ρ Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1)))
        (H β))
myFresh : ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
Fδ : List Formula × List Program
Fδ_in_Hβ : Fδ ∈ H β
h✝ : ¬Fδ.2 = []
⊢ (if Fδ.2 = [] then Formula.bottom else repl_in_F x ρ (Con ((~⌈⌈Fδ.2⌉⌉~·x) :: Fδ.1))) =
    if Fδ.2 = [] then Formula.bottom else Con ((~⌈⌈Fδ.2⌉⌉~ρ) :: Fδ.1)