fact: Definition sizes_lt l1 l2 := MultisetLt gt (sizes l1) (sizes l2).
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)