rw [disEval, helper]
case mp.beta_equiv.mp.intro.mk.intro.inl.refl.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
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 β
w_ : ∀ (f : Formula), f ∈ Fs ∨ f = (~~·x) → evaluate M w f
⊢ M.val w x ∧ evaluate M w (dis (List.map (fun x => if x.2 = [] then Con x.1 else Formula.bottom) (H β)))
case mp.beta_equiv.mp.intro.mk.intro.inl.refl.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
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 β
w_ : ∀ (f : Formula), f ∈ Fs ∨ f = (~~·x) → evaluate M w f
⊢ M.val w x ∧ ∃ Fδ ∈ H β, evaluate M w (if Fδ.2 = [] then Con Fδ.1 else Formula.bottom)