proposition: Lemma size2_lex2_mem : forall t f l s, mem equiv t l -> o_size2 (s,t) (s, Term f l).
proof: Proof. intros t f l s t_mem_l; destruct (mem_split_set _ _ equiv_bool_ok _ _ t_mem_l) as [t' [l1 [l2 [t_eq_t' [H _]]]]]. simpl in t_eq_t'; simpl in H. unfold o_size2, size2; rewrite (equiv_same_size t_eq_t'). apply (size2_lex2 t' f l s). subst l; apply in_or_app; right; left; 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)