simp [relateSeq]
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ relateSeq M (l :: l1 ++ l2) w v ↔ ∃ u, relateSeq M (l :: l1) w u ∧ relateSeq M l2 u v
W : Type
M : KripkeModel W
l2 : List Program
l : Program
l1 : List Program
IH : ∀ (w v : W), relateSeq M (l1 ++ l2) w v ↔ ∃ u, relateSeq M l1 w u ∧ relateSeq M l2 u v
w v : W
⊢ (∃ u, relate M l w u ∧ relateSeq M (l1 ++ l2) u v) ↔
    ∃ u, (∃ u_1, relate M l w u_1 ∧ relateSeq M l1 u_1 u) ∧ relateSeq M l2 u v