fact: Fixpoint intros_names (names : mlist name) : tactic := match names with | [m:] => idtac | name :m: names => T <- M.evar Type; intro_base name (fun x:T=>intros_names names) end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef