case inl hyp =>
  cases hyp
  subst_eqs
  simp_all [Yset]
  use w
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
Fs : List Formula
δ : List Program
w_Con : ∀ f ∈ Yset (Fs, δ) ψ, evaluate M w f
hyp : Fs = [] ∧ δ = []
⊢ evaluate M w (~⌈∗β⌉ψ)
no goals