proposition: Remark PrimRec_1_S (f: nat->nat) (g : nat -> nat -> nat -> nat) (i:nat): let phi := evalPrimRecFunc 1 f g in forall x, phi (S i) x = g i (phi i x) x.
proof: Proof. reflexivity. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)