{P : Sort u} →
  {r₁ : Aesop.ForwardRule} →
    {r₂ : Aesop.NormRule} →
      {r₁' : Aesop.ForwardRule} →
        {r₂' : Aesop.NormRule} →
          Aesop.BaseRuleSetMember.normForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.normForwardRule r₁' r₂' →
            (r₁ = r₁' → r₂ = r₂' → P) → P