proposition: Lemma evalListPrimrec_S : forall n (v: t nat n) (f : naryFunc n) (g : naryFunc (S (S n))) a, v_apply (evalPrimRecFunc _ f g) (cons (S a) v) = v_apply g (a :: v_apply (evalPrimRecFunc n f g) (a :: v) :: v).
proof: Proof. induction n. - intros; rewrite (t_0_nil _ v); now cbn. - intros; rewrite (decomp _ _ v); cbn. specialize (IHn (tl v)); cbn; rewrite evalListCompose2. cbn; auto. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)