proposition: Fact ra_enum_spec x v : ex (⟦ra_enum⟧ (x##v)) <-> exists n, ⟦f⟧ (n##v) (S x).
proof: Proof. Proof using Hf. unfold ra_enum; simpl; unfold s_min. rewrite μ_min_of_total. + split. * intros (r & Hr). destruct (Hg (r##x##v)) as (e & H1 & H2). simpl in H2. exists r; apply H2. revert H1 Hr; apply ra_rel_fun. * intros (n & Hn); exists n. destruct (Hg (n##x##v)) as (e & H1 & H2). apply H2 in Hn; subst; auto. + intros ? ? ?; apply ra_rel_fun. + intros y; destruct (Hg (y##x##v)) as (e & ? & _). exists e; auto. Qed.
imports: Arith Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_decidable pos vec) Undecidability.MuRec.Util(recalg ra_utils)