{ctx : Type u_1} →
  {P : Sort u} →
    {context context' : ctx} →
      Mathlib.TacticAnalysis.TriggerCondition.accept context = Mathlib.TacticAnalysis.TriggerCondition.accept context' →
        (context ≍ context' → P) → P