proposition: Fact nat_h10luc_surj lc : { k | lc = nat_h10luc k }.
proof: Proof. destruct (list_vec_full lc) as (v & <-). set (n := length lc). set (f p := match le_lt_dec n p with | left _ => (0,0,0) | right Hp => vec_pos v (nat2pos Hp) end). destruct godel_beta_fun_inv_triples with (n := n) (f := f) as (a & b & Hab). exists (recomp (recomp a b) n). unfold nat_h10luc. repeat (rewrite decomp_l_recomp). repeat rewrite decomp_r_recomp. rewrite map_pos_list_vec; f_equal. apply vec_pos_ext; intros p; rewrite vec_pos_set. unfold idx_h10uc; rewrite <- Hab; auto. 2: apply pos2nat_prop. unfold f, n. destruct (le_lt_dec (length lc) (pos2nat p)) as [ H | H ]. + generalize (pos2nat_prop p); lia. + rewrite nat2pos_pos2nat; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list crt pos vec) Undecidability.MuRec.Util(recalg ra_utils ra_enum recomp ra_recomp beta ra_godel_beta) Undecidability.DiophantineConstraints(H10C Util.h10c_utils)