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