simp_all [pairRel]
case h.right.a.cons.cons
W : Type
M : KripkeModel W
e : Program
v w u : W
v_d_u : relate M e v u
head✝¹ : W
tail✝¹ : List W
head✝ : Program
tail✝ : List Program
δ_notEmpty : ¬head✝ :: tail✝ = []
u_δ_w : relateSeq M (head✝ :: tail✝) u w
l_def : (head✝¹ :: tail✝¹).length + 1 = (head✝ :: tail✝).length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: (head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w]))
⊢ ∀ y ∈ ((head✝ :: tail✝).zip (head✝¹ :: tail✝¹ ++ [w])).head?, pairRel M (e, u) y
no goals