∀ (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)) (visibility : Lean.Elab.Visibility)
  (isProtected : Bool) (computeKind : Lean.Elab.ComputeKind) (recKind : Lean.Elab.RecKind) (isUnsafe : Bool)
  (attrs : Array Lean.Elab.Attribute) (stx_1 : Lean.TSyntax `Lean.Parser.Command.declModifiers)
  (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)) (visibility_1 : Lean.Elab.Visibility)
  (isProtected_1 : Bool) (computeKind_1 : Lean.Elab.ComputeKind) (recKind_1 : Lean.Elab.RecKind) (isUnsafe_1 : Bool)
  (attrs_1 : Array Lean.Elab.Attribute),
  ({ stx := stx, docString? := docString?, visibility := visibility, isProtected := isProtected,
        computeKind := computeKind, recKind := recKind, isUnsafe := isUnsafe, attrs := attrs } =
      { stx := stx_1, docString? := docString?_1, visibility := visibility_1, isProtected := isProtected_1,
        computeKind := computeKind_1, recKind := recKind_1, isUnsafe := isUnsafe_1, attrs := attrs_1 }) =
    (stx = stx_1 ∧
      docString? = docString?_1 ∧
        visibility = visibility_1 ∧
          isProtected = isProtected_1 ∧
            computeKind = computeKind_1 ∧ recKind = recKind_1 ∧ isUnsafe = isUnsafe_1 ∧ attrs = attrs_1)