proposition: Fact μ_min_of_total : (exists n, μ_min n) <-> exists x, R x 0.
proof: Proof. Proof using Rfun HR. split. + intros (n & ? & _); exists n; auto. + intros H. destruct first_which_ni with (2 := H) as (n & H1 & H2). * intros n; destruct (HR n) as ([ | k] & Hk); auto. right; intros C; generalize (Rfun Hk C); discriminate. * exists n; split; auto. intros i Hi; apply H2 in Hi. destruct (HR i) as ([ | k] & Hk); try tauto. exists k; 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