∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin p.length) (a : α)
  (prev_connect : (p.toFun i.castSucc, a) ∈ r) (connect_next : (a, p.toFun i.succ) ∈ r),
  (p.insertNth i a prev_connect connect_next).length = p.length + 1