{P : Sort u} →
  {fvarId : Lean.FVarId} →
    {idx : ℕ} →
      {fvarId' : Lean.FVarId} →
        {idx' : ℕ} →
          { fvarId := fvarId, idx := idx } = { fvarId := fvarId', idx := idx' } →
            (fvarId = fvarId' → idx = idx' → P) → P