proposition: Remark PrimRec_0_S (a : nat) (g : nat -> nat -> nat) (i:nat): let phi := evalPrimRecFunc 0 a g in phi (S i) = g i (phi i).
proof: Proof. reflexivity. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)