∀ (ref : Lean.Syntax) (attrs : Array Lean.Elab.Attribute) (shortDeclName declName : Lean.Name)
  (parentName? : Option Lean.Name) (binderIds : Array Lean.Syntax) (binders : Lean.Syntax) (type mvar : Lean.Expr)
  (valStx : Lean.Syntax) (termination : Lean.Elab.TerminationHints)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)) (ref_1 : Lean.Syntax)
  (attrs_1 : Array Lean.Elab.Attribute) (shortDeclName_1 declName_1 : Lean.Name) (parentName?_1 : Option Lean.Name)
  (binderIds_1 : Array Lean.Syntax) (binders_1 : Lean.Syntax) (type_1 mvar_1 : Lean.Expr) (valStx_1 : Lean.Syntax)
  (termination_1 : Lean.Elab.TerminationHints)
  (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment × Bool)),
  ({ ref := ref, attrs := attrs, shortDeclName := shortDeclName, declName := declName, parentName? := parentName?,
        binderIds := binderIds, binders := binders, type := type, mvar := mvar, valStx := valStx,
        termination := termination, docString? := docString? } =
      { ref := ref_1, attrs := attrs_1, shortDeclName := shortDeclName_1, declName := declName_1,
        parentName? := parentName?_1, binderIds := binderIds_1, binders := binders_1, type := type_1, mvar := mvar_1,
        valStx := valStx_1, termination := termination_1, docString? := docString?_1 }) =
    (ref = ref_1 ∧
      attrs = attrs_1 ∧
        shortDeclName = shortDeclName_1 ∧
          declName = declName_1 ∧
            parentName? = parentName?_1 ∧
              binderIds = binderIds_1 ∧
                binders = binders_1 ∧
                  type = type_1 ∧
                    mvar = mvar_1 ∧ valStx = valStx_1 ∧ termination = termination_1 ∧ docString? = docString?_1)