proposition: Lemma List_cons_inj : forall {A} {h1 h2} {t1 t2: list A}, h1 :: t1 = h2 :: t2 -> h1 = h2 /\ t1 = t2.
proof: Proof. inversion 1; intuition congruence. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics