proposition: Lemma combine_inv : forall A B input output combined, List.length input = List.length output -> @List.combine A B input output = combined -> input = fst (List.split combined) /\ output = snd (List.split combined).
proof: Proof. intros; subst; rewrite List.combine_split; intuition eauto. Qed.
imports: Coq.Lists.List CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics