proposition: Lemma size2_lex1_mem : forall s f l t1 t2, mem equiv s l -> o_size2 (s,t1) (Term f l,t2).
proof: Proof. intros s f l t1 t2 s_mem_l; destruct (mem_split_set _ _ equiv_bool_ok _ _ s_mem_l) as [s' [l1 [l2 [s_eq_s' [H _]]]]]. simpl in s_eq_s'; simpl in H. unfold o_size2, size2; rewrite (equiv_same_size s_eq_s'). apply (size2_lex1 s' f l t1 t2). 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)