(motive : List Lean.MVarId × List Lean.MVarId → Sort u_1) →
  (x : List Lean.MVarId × List Lean.MVarId) →
    ((mvarIdsCoherence mvarIdsRefl : List Lean.MVarId) → motive (mvarIdsCoherence, mvarIdsRefl)) → motive x