proposition: Lemma plus_correct: PRcorrect plus Nat.add.
proof: Proof. intros n; induction n as [ | n IHn]. - intro; reflexivity. - intro p; cbn in IHn |- *; now rewrite IHn. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)