proposition: Fact ra_comp_tot : total [|ra_comp f g|].
proof: Proof. Proof using Hf Hg. intros v. assert (H1 : forall p, exists x, [|vec_pos g p|] v x) by (intro; apply Hg). apply vec_reif in H1; destruct H1 as (w & Hw). destruct (Hf w) as (y & Hy). exists y, w; split; auto. intro; rewrite vec_pos_set; 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