proposition: Fact μ_min_fun n m : μ_min n -> μ_min m -> n = m.
proof: Proof. Proof using Rfun. intros (H1 & H2) (H3 & H4). destruct (lt_eq_lt_dec n m) as [ [ H | ] | H ]; auto; [ apply H4 in H | apply H2 in H ]; destruct H as (u & Hu); [ generalize (Rfun H1 Hu) | generalize (Rfun H3 Hu) ]; discriminate. Qed.
imports: Arith Lia List Bool Eqdep_dec Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.MuRec.MuRec