proposition: Fact nat_h10lc_surj lc : { k | lc = nat_h10lc k }.
proof: Proof. destruct (list_vec_full lc) as (v & <-). generalize (length lc) v; clear lc v. intros n v. set (w := vec_map h10c_nat v). destruct beta_inv with (v := w) as (lc & Hlc). exists (recomp n lc). unfold nat_h10lc. rewrite decomp_l_recomp. rewrite map_pos_list_vec; f_equal. apply vec_pos_ext; intros p. rewrite vec_pos_set, decomp_r_recomp, Hlc. unfold w; rewrite vec_pos_map, nat_h10c_nat. 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)