proposition: Theorem ra_univ_spec : ex (⟦ra_univ⟧ (k##vec_nil)) <-> exists φ, forall c, In c lc -> h10c_sem c φ.
proof: Proof. Proof using Hf_tot. split. + intros (v & Hv). simpl in Hv; red in Hv. destruct Hv as (H1 & H2). destruct (h10lc_sem_dec lc (beta v)) as [ (c & H) | H ]. * assert (⟦ f ⟧ (v ## k ## vec_nil) 1) as C. { apply Hf_val_1; exists c; auto. } generalize (ra_rel_fun _ _ _ _ H1 C); discriminate. * exists (beta v); auto. + intros (phi & Hphi). destruct (beta_fun_inv (h10lc_bound lc) phi) as (v & Hv). generalize (h10lc_bound_prop _ _ Hv); clear Hv; intros Hv. apply ra_min_ex; auto. exists v; simpl. apply Hf_val_0. intros c Hc; apply Hv; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat utils_list) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recalg ra_utils ra_enum recomp ra_recomp beta ra_godel_beta) Undecidability.DiophantineConstraints(H10C Util.h10c_utils)