fact: Definition find_in_constrs {C} (c : C) : mlist dyn -> M (mlist dyn) := mfix1 f (cs : _) : M _ := match cs with | mnil => M.ret mnil | mcons c' cs => '(m: c, _) <- M.decompose c; dcase c as C, c in let C := reduce (RedVmCompute) C in mmatch c' with | @Dyn C c =n> M.ret cs | _ => l <- f cs; M.ret (c' :m: l) end end.
imports: Mtac2(Base List Datatypes)