proposition: Lemma cPairInj2 a b c d : cPair a b = cPair c d -> b = d.
proof: Proof. intro H; assert (H0: a + b = c + d) by ( apply cPairInjHelp; auto ). assert (H1: a = c) by (eapply cPairInj1; apply H). rewrite H1 in H0; now rewrite Nat.add_cancel_l in H0. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec)