simp only [relate] at v_γ_w
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α;'β) v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w