{P : Sort u} →
  {rule : Aesop.SafeRule} →
    {output : Aesop.RuleTacOutput} →
      {rule' : Aesop.SafeRule} →
        {output' : Aesop.RuleTacOutput} →
          { rule := rule, output := output } = { rule := rule', output := output' } →
            (rule = rule' → output = output' → P) → P