fact: Fixpoint remove_not_common (acc l1 l2 : list elt) {struct l2} : list elt := match l2 with | nil => acc | e :: l => if In_dec eq_elt_dec e l1 then remove_not_common (e :: acc) l1 l else remove_not_common acc l1 l end.
imports: List more_list list_permut Arith