fact: Fixpoint zip(A B : Set)(lsa : list A)(lsb : list B) := match lsa with | nil => nil | a :: lsa' => match lsb with | nil => nil | b :: lsb' => (a, b) :: (zip lsa' lsb') end end.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool