case inl δ_eq_empty =>
  subst δ_eq_empty
  intro _
  simp_all [pairRel]
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
δ_eq_empty : δ = []
⊢ relateSeq M (e :: δ) v w →
    e :: δ ≠ [] → ∃ l, l.length + 1 = (e :: δ).length ∧ List.Chain' (pairRel M) (((?'⊤) :: e :: δ).zip (v :: l ++ [w]))
no goals