case inl v_is_w =>
  subst v_is_w
  use []
  simp_all [P,relateSeq]
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
ℓ : TP (∗β)
v_conF : (M, v)⊨Con (F (∗β) ℓ)
v_γ_w : Relation.ReflTransGen (relate M β) v w
v_is_w : v = w
⊢ ∃ δ ∈ P (∗β) ℓ, relateSeq M δ v w
no goals