fact: Definition first {B} : mlist (gtactic B) -> gtactic B := fix go l : gtactic B := match l with | [m:] => T.raise NoProgress | x :m: xs => x || go xs end.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic Sorts MTeleMatch) Strings.String NArith.BinNat NArith.BinNatDef