simp_all [pairRel]
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: u :: l ++ [w]))
case h.right
W : Type
M : KripkeModel W
e : Program
δ : List Program
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
l : List W
l_def : l.length + 1 = δ.length
lchain : List.Chain' (pairRel M) ((?'(~Formula.bottom), u) :: δ.zip (l ++ [w]))
⊢ List.Chain' (pairRel M) ((e, u) :: δ.zip (l ++ [w]))