fact: Definition cmp f g := match f, g with | Rec u, Rec v => Ty_Cmp.cmp u v | _, _ => Nat.compare (prec f) (prec g) end.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec)