rw [relateSeq_append]
case h.right.right
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
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M (Fs, δ ++ [∗β]).2 v w
case h.right.right
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
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ u, relateSeq M δ v u ∧ relateSeq M [∗β] u w