fact: Definition fapp {A B} (f : gtactic (A -> B)) (x : gtactic A) : gtactic B := bind f (fun g => fmap g x).
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef