proposition: Lemma wf_lt : well_founded lt.
proof: Proof. unfold lt. apply WF_wf_transp. apply WF_lex. apply wf_WF_transp. exact wf_nb_vars_lt. apply wf_WF_transp. exact wf_sizes_lt. unfold RelationClasses.Transitive, nb_vars_eq. intros. trans (cardinal (vars_eqns y)); hyp. unfold inclusion, transp, nb_vars_eq, nb_vars_lt. intros. do 2 destruct H. rewrite H. hyp. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)