Library MetaRocq.Utils.MRTactics.SpecializeAllWays

Require Export MetaRocq.Utils.MRTactics.UniquePose.

Ltac specialize_all_ways :=
  repeat match goal with
         | [ H : ?A, H' : ∀ a : ?A, _ |- _ ]
           ⇒ unique pose proof (H' H)
         end.