use w
case intro.refl.refl
ψ : Formula
β : Program
ρ : Formula := dis (List.map (fun Fδ => Con (Yset Fδ ψ)) (H (∗β)))
W : Type
M : KripkeModel W
w : W
w_Con : ¬evaluate M w ψ
⊢ ∃ x, Relation.ReflTransGen (relate M β) w x ∧ ¬evaluate M x ψ
no goals