fact: Definition bpermut := forallb (fun f => bforall_lt (fun i => mem beq_nat i (raw_pi f)) (arity f)) Fs.
imports: CoLoR(LogicUtil ATrs ListUtil NatUtil VecUtil SN BoolUtil RelUtil ListNodup VecFilterPerm ARelation ACompat NaryFunction BoundNat ListDec)