proposition: Lemma codeListInj (l m : list nat): codeList l = codeList m -> l = m.
proof: Proof. revert m; induction l as [| a l Hrecl]. - intros m H; destruct m as [| n l]. + reflexivity. + discriminate H. - intros m H; destruct m as [| n l0]. + discriminate H. + simpl in H. replace n with a. * rewrite (Hrecl l0); [reflexivity |]. eapply cPairInj2; apply eq_add_S, H. * eapply cPairInj1; apply eq_add_S, H. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction