proposition: Fact prim_rec_tot k f : @prim_rec k f -> total [|f|].
proof: Proof. induction f as [ x | | | n p | n i f g Hf Hg | n f g Hf Hg | n f Hf ]; intros H; simpl in H; auto. + apply ra_comp_tot; try tauto; intros; apply Hg, H. + apply ra_rec_tot; tauto. + tauto. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec