proposition: Lemma cTripleProj (a: nat) : cTriple (cTriplePi1 a) (cTriplePi2 a) (cTriplePi3 a) = a.
proof: Proof. unfold cTriple, cTriplePi1, cTriplePi2, cTriplePi3; repeat rewrite cPairProjections; reflexivity. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction