proposition: Lemma evalListComp : forall n (v: t nat n) m (gs: t (naryFunc n) m) (h: naryFunc m), v_apply (evalComposeFunc _ _ gs h) v = v_apply h (map (fun g => v_apply g v) gs).
proof: Proof. induction n. - intros; rewrite (t_0_nil _ v); cbn. induction m. + rewrite (t_0_nil _ gs); cbn; auto. + rewrite (decomp _ _ gs); cbn. simpl naryFunc in *. specialize (IHm (tl gs) (h (vfst gs))); now rewrite IHm. - intros; induction m. + rewrite (t_0_nil _ gs); cbn. rewrite (decomp _ _ v); cbn. specialize (IHn (tl v) 0 (nil) h); rewrite IHn; cbn; auto. + rewrite (decomp _ _ v). rewrite (decomp _ _ gs). specialize (IHm (tl gs)); cbn. specialize (IHn (tl v)); rewrite IHn; cbn. f_equal; f_equal. generalize m gs; intro m0; induction m0. * cbn; intros; rewrite (decomp1 gs0); cbn; auto. * intros; replace gs0 with (cons (hd gs0) (cons (hd (tl gs0)) (tl (tl gs0)))). -- cbn; cbn in *; specialize (IHm0 (tl gs0)); rewrite IHm0; auto. -- rewrite decomp; f_equal. now rewrite decomp. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)