fact: Parameter permut_bool_ok : forall l1 l2, match permut_bool l1 l2 with true => permut l1 l2 | false => ~permut l1 l2 end.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)