rcases hyp with ⟨_, ⟨v1, v_neq_v1, v_β_v1, v1_βS_w⟩⟩
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
hyp : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w