proposition: Lemma cTripleProj2 (a b c : nat) : cTriplePi2 (cTriple a b c) = b.
proof: Proof. unfold cTriplePi2, cTriple; rewrite cPairProjections2; apply cPairProjections1. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction