proposition: Lemma s_rec_fun f h : functional f -> functional h -> functional (s_rec f h).
proof: Proof. intros Hf Hh ? ? ?. apply μ_rec_fun. + apply Hf. + intros ? ? ? ? ?; apply Hh; auto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec