proposition: Fact ra_iter_n_val i v : ⟦ra_iter_n⟧ (i##v) (iter (g v) i (f v)).
proof: Proof. Proof using Hf Hg. simpl; unfold s_rec. induction i as [ | i IHi ]; simpl; auto. exists (iter (g v) i (f v)); split; auto. exists (iter (g v) i (f v)## v); split; auto. intros p; analyse_pos p; simpl; auto. vec pos simpl. 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)