{P : Sort u} →
  {target : Aesop.CasesTarget} →
    {md : Lean.Meta.TransparencyMode} →
      {isRecursiveType : Bool} →
        {ctorNames : Array Aesop.CtorNames} →
          {target' : Aesop.CasesTarget} →
            {md' : Lean.Meta.TransparencyMode} →
              {isRecursiveType' : Bool} →
                {ctorNames' : Array Aesop.CtorNames} →
                  Aesop.RuleTacDescr.cases target md isRecursiveType ctorNames =
                      Aesop.RuleTacDescr.cases target' md' isRecursiveType' ctorNames' →
                    (target = target' → md = md' → isRecursiveType = isRecursiveType' → ctorNames = ctorNames' → P) → P