proposition: Lemma size3_lex2_mem : forall t f l s u1 u2, mem equiv t l -> o_size3 (s,(t,u1)) (s,(Term f l, u2)).
proof: Proof. intros t f l s u1 u2 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_size3, size3, size2; rewrite (equiv_same_size t_eq_t'). apply (size3_lex2 t' f l s u1 u2). 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)