proposition: Fact ra_iter_val k x : ⟦ra_iter⟧ (k##x##vec_nil) (iter f k x).
proof: Proof. Proof using Hf. unfold ra_iter. rewrite ra_iter_n_rel with (f := @vec_head _ _) (g := fun _ => f); simpl; auto. + intros v; vec split v with y; vec nil v; auto. + intros i v; vec split v with y; vec nil v; simpl; auto. exists (i##vec_nil); split; auto. * rewrite Hf; auto. * pos split; simpl; auto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)