proposition: Fact ra_iter_h10c_val_0 : (forall p, p < n -> h10c_sem (nat_h10c (beta lc p)) (beta v)) -> ⟦ra_iter_h10c⟧ (n##lc##v##vec_nil) 0.
proof: Proof. intros H2; simpl. exists (1##vec_nil); split. { apply ra_not_val. } pos split; simpl; auto. exists (0##vec_nil); split. { apply ra_not_val. } pos split; simpl; auto. apply ra_lsum_0. intros p Hp. specialize (H2 _ Hp). apply h10c_test_spec in H2. rewrite h10c_test_stable in H2. rewrite <- H2. apply Hf_val. 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)