proposition: Fact ra_rec_tot n f g : total [|f|] -> total [|g|] -> total [|@ra_rec n f g|].
proof: Proof. intros Hf Hg v; vec split v with x. simpl; induction x as [ | x IHx ]; simpl. + destruct (Hf v) as (y & Hy). exists y; red; simpl; auto. + destruct IHx as (y & Hy). destruct (Hg (x##y##v)) as (z & Hz). exists z, y; simpl; split; 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