proposition: Remark PrimRec_2_S (f: naryFunc 2) (g : naryFunc 4) (i:nat) : let phi := evalPrimRecFunc 2 f g in forall x y, phi (S i) x y = g i (phi i x y) x y.
proof: Proof. reflexivity. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)