{P : Sort u} →
  {declName : Lean.Name} →
    {post : Bool} →
      {keys : Array Lean.Meta.SimpTheoremKey} →
        {declName' : Lean.Name} →
          {post' : Bool} →
            {keys' : Array Lean.Meta.SimpTheoremKey} →
              { declName := declName, post := post, keys := keys } =
                  { declName := declName', post := post', keys := keys' } →
                (declName = declName' → post = post' → keys = keys' → P) → P