∀ {self : Batteries.UnionFind} {x y : Fin self.size},
  self.parent ↑x = ↑x →
    self.parent ↑y = ↑y →
      ∀ {m : Batteries.UnionFind},
        (∀ (i : ℕ), m.parent i = if ↑y = i then ↑x else self.parent i) →
          ∀ (i : ℕ), m.rootD i = if self.rootD i = ↑x ∨ self.rootD i = ↑y then ↑x else self.rootD i