specialize IH u_δ_w δ_notEmpty
case intro.intro
W : Type
M : KripkeModel W
e : Program
δ : List Program
IH :
  ∀ {v w : W},
    relateSeq M δ v w →
      δ ≠ [] → ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (v :: l ++ [w]))
v w : W
δ_notEmpty : ¬δ = []
u : W
v_d_u : relate M e v u
u_δ_w : relateSeq M δ u w
a✝ : e :: δ ≠ []
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
case intro.intro
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 :: δ ≠ []
IH : ∃ l, l.length + 1 = δ.length ∧ List.Chain' (pairRel M) (((?'⊤) :: δ).zip (u :: l ++ [w]))
⊢ ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))