fact: Definition enum_Decr := flat_map (fun f => map (fun x : L f * L f => let (a,b) := x in decr a b) (L2s f)) Fs.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)