fact: Fixpoint combine A (l : list (A * A)) (l1 l2 : list A) {struct l1} : list (A * A) := match l1, l2 with | nil, _ => l | _, nil => l | (a1 :: l1), (a2 :: l2) => combine _ ((a1,a2) :: l) l1 l2 end.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)