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