proposition: Lemma s_min_fun g : functional g -> functional (s_min g).
proof: Proof. intros Hg ? ? ?; apply μ_min_fun. intros ? ? ?; apply Hg. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec