fact: Definition do_intro : LIP -> tactic := mfix2 do_intro (lip : LIP) (g : goal gs_open) : M (mlist (unit *m goal gs_any)) := (match lip return tactic with | lnil => T.idtac | lcons ip lnil => to_tactic ip do_intro | lcons ip lip => to_tactic ip do_intro ;; do_intro lip end%tactic) g.
imports: Coq.Strings.String Mtac2(List Base) Mtac2.tactics(TacticsBase Tactics ImportedTactics)