{P : Sort u_1} →
  {coll : Type u} →
    {idx : Type v} →
      {elem : Type w} →
        {valid : coll → idx → Prop} →
          {t : GetElem coll idx elem valid} →
            {coll' : Type u} →
              {idx' : Type v} →
                {elem' : Type w} →
                  {valid' : coll' → idx' → Prop} →
                    {t' : GetElem coll' idx' elem' valid'} →
                      coll = coll' →
                        idx = idx' → elem = elem' → valid ≍ valid' → t ≍ t' → GetElem.noConfusionType P t t'