simp_all [P,relateSeq]
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ [] ∈ P (∗β) ℓ ∧ relateSeq M [] v v
no goals