proposition: Lemma Lt_cons : forall x l, Lt l (x :: l).
proof: Proof. intros. unfold Lt, lt, transp. apply lex_intro. unfold nb_vars_eq, nb_vars_lt. simpl. set (X := vars_eqns l). set (Y := vars_eqn x). assert (cardinal X <= cardinal (XSet.union Y X)). apply subset_cardinal. intro; set_iff; tauto. case (eq_nat_dec (cardinal X) (cardinal (XSet.union Y X))); intro. right. split_all. unfold sizes_lt. unfold sizes. simpl. unfold MultisetLt, transp. apply t_step. set (M := list2multiset (map size l)). apply MSetRed with (X := M) (a := size x) (Y := MSetCore.empty). solve_meq. solve_meq. intros. apply False_rec. eapply not_empty. apply H0. refl. left. lia. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)