{P : Sort u} →
  {name : Aesop.RuleName} →
    {pattern : Aesop.RulePattern} →
      {name' : Aesop.RuleName} →
        {pattern' : Aesop.RulePattern} →
          { name := name, pattern := pattern } = { name := name', pattern := pattern' } →
            (name = name' → pattern = pattern' → P) → P