proposition: Theorem s_rec_eq f h v x : s_rec f h v x <-> exists s, f (vec_tail v) (s 0) /\ s (vec_head v) = x /\ forall i, i < vec_head v -> h (i##s i##vec_tail v) (s (S i)).
proof: Proof. vec split v with n; apply μ_rec_eq. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec