fact: Definition index {A} (c: A) : M _ := l <- get_constrs A; (mfix2 f (i : nat) (l : mlist dyn) : M nat := mmatch l with | [? l'] (Dyn c :m: l') => M.ret i | [? d' l'] (d' :m: l') => f (S i) l' end)%MC 0 l.
imports: Coq.Strings.String Mtac2(Datatypes List Mtac2)