fact: Definition μ_min n := R n 0 /\ forall i, i < n -> exists u, R i (S u).
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec