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