fact: Definition lhs_fun l r (_ : rule l r) := match head l with | Def.Fun f => f | _ => Zero end.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite)