proposition: Lemma wf_sizes_lt : well_founded sizes_lt.
proof: Proof. unfold sizes_lt. apply wf_inverse_image with (B := Multiset). apply mord_wf. unfold eqA. intros. subst. compute. lia. exact lt_wf. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)