proposition: Fact μ_rec_fun : functional μ_rec.
proof: Proof. Proof using Ffun Gfun. intros n; induction n as [ | n IHn ]; simpl; auto. intros x y (a & H1 & H2) (b & H3 & H4). specialize (IHn _ _ H1 H3); subst b. revert H2 H4; apply Gfun. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec