{P : Sort u} →
  {val : Lean.Expr} →
    {synthOrder : Array ℕ} →
      {val' : Lean.Expr} →
        {synthOrder' : Array ℕ} →
          { val := val, synthOrder := synthOrder } = { val := val', synthOrder := synthOrder' } →
            (val = val' → synthOrder = synthOrder' → P) → P