fact: Fixpoint zip {A B} (a: list A) (b: list B): list (A * B) := match a, b with | ah :: au, bh :: bt => (ah, bh) :: zip au bt | _, _ => nil end.
imports: Coq.Lists.List Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms CoRN.stdlib_omissions.Pair