fact: Fixpoint combine A B (r:list A) (s:list B) : list (A*B) := match r, s with | nil, nil => nil | a::r', b::s' => (a,b)::(combine r' s') | _, _ => arbitrary end.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)