proposition: Fact h10c_test_stable c v : h10c_test (h10c_nat (nat_h10c c)) v = h10c_test c v.
proof: Proof. unfold h10c_test, h10c_nat, nat_h10c. destruct (decomp_l c) as [ | [] ]; 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)