fact: Definition permut_bool := (fix permut_bool (kk1 kk2 : list A) {struct kk1} : bool := (match kk1 with | nil => match kk2 with nil => true | _ :: _=> false end | t1 :: k1 => match remove EDS1.eq_bool t1 kk2 with None => false | Some k2 => permut_bool k1 k2 end end)).
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)