{P : Sort u} →
  {toBaseRuleSet : Aesop.BaseRuleSet} →
    {simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems)} →
      {simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size} →
        {simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs)} →
          {simprocsArrayNonempty : 0 < simprocsArray.size} →
            {localNormSimpRules : Array Aesop.LocalNormSimpRule} →
              {toBaseRuleSet' : Aesop.BaseRuleSet} →
                {simpTheoremsArray' : Array (Lean.Name × Lean.Meta.SimpTheorems)} →
                  {simpTheoremsArrayNonempty' : 0 < simpTheoremsArray'.size} →
                    {simprocsArray' : Array (Lean.Name × Lean.Meta.Simprocs)} →
                      {simprocsArrayNonempty' : 0 < simprocsArray'.size} →
                        {localNormSimpRules' : Array Aesop.LocalNormSimpRule} →
                          { toBaseRuleSet := toBaseRuleSet, simpTheoremsArray := simpTheoremsArray,
                                simpTheoremsArrayNonempty := simpTheoremsArrayNonempty, simprocsArray := simprocsArray,
                                simprocsArrayNonempty := simprocsArrayNonempty,
                                localNormSimpRules := localNormSimpRules } =
                              { toBaseRuleSet := toBaseRuleSet', simpTheoremsArray := simpTheoremsArray',
                                simpTheoremsArrayNonempty := simpTheoremsArrayNonempty',
                                simprocsArray := simprocsArray', simprocsArrayNonempty := simprocsArrayNonempty',
                                localNormSimpRules := localNormSimpRules' } →
                            (toBaseRuleSet = toBaseRuleSet' →
                                simpTheoremsArray = simpTheoremsArray' →
                                  simprocsArray = simprocsArray' → localNormSimpRules = localNormSimpRules' → P) →
                              P