proposition: Fact μ_min_eq n : μ_min n <-> R n 0 /\ exists s, forall i, i < n -> R i (S (s i)).
proof: Proof. unfold μ_min; split; intros [ H0 H ]; split; auto. + apply fin_reif_nat with (1 := H). + clear H0; destruct H as (s & Hs). intros i ?; exists (s i); 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