∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (self : h.WeakRankFunction α)
  {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → self.rank x < self.rank y