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