fact: Definition use {A} (t : tactic) : ttac A := '(m: a, g) <- to_goal A; gs <- t g; let gs := dreduce (@mmap) (mmap (fun '(m: _, g) => g) gs) in M.ret (m: a, gs).
imports: Mtac2(Base Datatypes List Sorts tactics.Tactics) Strings.String