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