proposition: Lemma nat_h10c_nat c : nat_h10c (h10c_nat c) = c.
proof: Proof. destruct c; simpl; unfold nat_h10c; repeat (rewrite decomp_l_recomp || rewrite decomp_r_recomp); 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)