fact: Definition unfold_in {A B} (x : A) (h : B) : tactic := reduce_in (RedStrong [rl:RedBeta; RedMatch; RedFix; RedDeltaOnly [rl:Dyn x]]) h.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef