simp
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ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
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = [(Fs, δ ++ [∗β])]) ∧
    (Fs, δ ++ [∗β]) ∈ [(Fs, δ ++ [∗β])]
case h
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
x : ℕ := freshVarProg β
σ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
Fs : List Formula
δ : List Program
v : W
right_to_left_claim :
  ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w ρ → ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
x_not_in : x ∉ voc β
Fδ_in : (Fs, δ) ∈ H β
hyp : ¬δ = []
repl_w_ : ¬evaluate M w (⌈⌈δ⌉⌉~ρ) ∧ ∀ a ∈ Fs, evaluate M w a
w_ρ_v : relateSeq M δ w v
v_ρ : evaluate M v ρ
⊢ ∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = [(Fs, δ ++ [∗β])]