proposition: Lemma size3_lex3_mem_preceq : forall u f g h l l' s, mem equiv u l -> prec_eq Prec g h -> o_size3 (s,(Term g l',u)) (s,(Term h l',Term f l)).
proof: Proof. intros u f g h l l' s u_mem_l; destruct (mem_split_set _ _ equiv_bool_ok _ _ u_mem_l) as [u' [l1 [l2 [u_eq_u' [H _]]]]]. simpl in u_eq_u'; simpl in H. unfold o_size3, size3, size2; rewrite (equiv_same_size u_eq_u'). intros prec_g_h. apply (size3_lex3_prec u' f g h l l' s). subst l; apply in_or_app; right; left; trivial. trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)