proposition: Theorem ra_min_ex : ex (⟦ra_min f⟧ v) <-> exists x, ⟦f⟧ (x##v) 0.
proof: Proof. Proof using Hf. apply ra_min_extra. intros x; destruct (Hf x); firstorder. Qed.
imports: Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_decidable pos vec) Undecidability.MuRec.Util(recalg ra_utils)