simp_all [pairRel]
W : Type
M : KripkeModel W
e : Program
v w : W
IH :
  ∀ {v w : W},
    relateSeq M [] v w → [] ≠ [] → ∃ l, l.length + 1 = [].length ∧ List.Chain' (pairRel M) ([?'⊤].zip (v :: l ++ [w]))
a✝ : relateSeq M [e] v w
⊢ [e] ≠ [] → ∃ l, l.length + 1 = [e].length ∧ List.Chain' (pairRel M) ([?'⊤, e].zip (v :: l ++ [w]))
no goals