{motive : Aesop.NormM.Context → Sort u} →
  ((options : Aesop.Options') →
      (ruleSet : Aesop.LocalRuleSet) →
        (normSimpContext : Aesop.NormSimpContext) →
          motive { options := options, ruleSet := ruleSet, normSimpContext := normSimpContext }) →
    (t : Aesop.NormM.Context) → motive t