proposition: Lemma cst_correct (k:nat) : PRcorrect (cst k) (fun _ => k).
proof: Proof. induction k as [| k IHk]; simpl; intros p. - reflexivity. - cbn; now rewrite IHk. Qed.
imports: Coq(Arith ArithRing List Vector Utf8) hydras(primRec cPair)