fact: Fixpoint name_pattern (l : list (list string)) : mlist tactic := match l with | nil => [m:] | ns :: l => intros_simpl ns :m: name_pattern l end%list.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef