proposition: Lemma Lt_combine : forall f vs g us l, beq_symb f g = true -> Lt (combine (list_of_vec vs) (list_of_vec us) ++ l) ((Fun f vs, Fun g us) :: l).
proof: Proof. intros. unfold Lt, lt, transp. apply lex_intro. right. split. unfold nb_vars_eq, nb_vars_lt. simpl. unfold vars_eqn, fst, snd. rewrite !vars_fun, vars_eqns_app. rewrite beq_symb_ok in H. subst. rewrite vars_eqns_combine. refl. unfold sizes_lt, MultisetLt, transp. apply t_step. unfold sizes. simpl. rewrite map_app. set (M := list2multiset (map size l)). apply MSetRed with (X := M) (a := size (Fun f vs, Fun g us)) (Y := list2multiset (map size (combine (list_of_vec vs) (list_of_vec us)))). solve_meq. rewrite list2multiset_app. unfold M. solve_meq. intros. unfold size, fst, snd. rewrite !nb_symb_occs_fun. destruct (member_multiset_list _ H0). destruct (in_map_elim H1). destruct H3. subst. destruct x0. ded (in_combine_l H3). ded (in_combine_r H3). ded (in_list_of_vec H4). ded (in_list_of_vec H5). ded (Vin_nb_symb_occs_terms_ge H6). ded (Vin_nb_symb_occs_terms_ge H7). rewrite H2. unfold size, fst, snd. lia. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)