∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι]
  [inst_2 : (i : ι) → LinearOrder (α i)] (f g : Π₀ (i : ι), α i) (wit : ι),
  (f.neLocus g).min = ↑wit →
    g wit < f wit →
      ∃ i, (∀ j < i, (ofLex (toLex g)) j = (ofLex (toLex f)) j) ∧ (ofLex (toLex g)) i < (ofLex (toLex f)) i