{R : Type u} →
  {ι : Type u_4} →
    {M : Type u_5} →
      {motive : exteriorPower.presentation.Rels R ι M → Sort u_1} →
        (ctorIdx : ℕ) →
          (t : exteriorPower.presentation.Rels R ι M) →
            ctorIdx = t.ctorIdx → exteriorPower.presentation.Rels.ctorElimType ctorIdx → motive t