proposition: Lemma size3_lex3_mem : forall u f l s t, mem equiv u l -> o_size3 (s,(t,u)) (s,(t,Term f l)).
proof: Proof. intros u f l s t 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'). apply (size3_lex3 u' f l s t). 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)