proposition: Lemma wf_Lt : well_founded Lt.
proof: Proof. unfold Lt. apply wf_inverse_image with (f := fun l : eqns => (l, l)). exact wf_lt. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)