{α : Sort u} →
  {P : Sort u_1} →
    {op : α → α → α} →
      {assoc : Std.Associative op} →
        {comm : Option (PLift (Std.Commutative op))} →
          {idem : Option (PLift (Std.IdempotentOp op))} →
            {vars : List (Lean.Data.AC.Variable op)} →
              {arbitrary : α} →
                {op' : α → α → α} →
                  {assoc' : Std.Associative op'} →
                    {comm' : Option (PLift (Std.Commutative op'))} →
                      {idem' : Option (PLift (Std.IdempotentOp op'))} →
                        {vars' : List (Lean.Data.AC.Variable op')} →
                          {arbitrary' : α} →
                            { op := op, assoc := assoc, comm := comm, idem := idem, vars := vars,
                                  arbitrary := arbitrary } =
                                { op := op', assoc := assoc', comm := comm', idem := idem', vars := vars',
                                  arbitrary := arbitrary' } →
                              (op ≍ op' → comm ≍ comm' → idem ≍ idem' → vars ≍ vars' → arbitrary ≍ arbitrary' → P) → P