∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  {dropping : Bool} {inner : Std.IterM m β} {dropping_1 : Bool} {inner_1 : Std.IterM m β},
  { dropping := dropping, inner := inner } = { dropping := dropping_1, inner := inner_1 } →
    dropping = dropping_1 ∧ inner = inner_1