∀ {α : 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)