{P : Sort u} →
  {α : Type w} →
    {m : Type w → Type w'} →
      {β : Type w} →
        {inst : Std.Iterator α m β} →
          {P_1 : β → Prop} →
            {t : Std.Iterators.Types.Attach α m P_1} →
              {α' : Type w} →
                {m' : Type w → Type w'} →
                  {β' : Type w} →
                    {inst' : Std.Iterator α' m' β'} →
                      {P' : β' → Prop} →
                        {t' : Std.Iterators.Types.Attach α' m' P'} →
                          α = α' →
                            m = m' →
                              β = β' →
                                inst ≍ inst' → P_1 ≍ P' → t ≍ t' → Std.Iterators.Types.Attach.noConfusionType P t t'