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