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