proposition: Lemma size_direct_subterm_mem : forall n t f l, size (Term f l) <= S n -> mem equiv t l -> size t <= n.
proof: Proof. intros n t f l Sfl t_mem_l; apply le_S_n. apply Nat.le_trans with (size (Term f l)); trivial. 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; subst l. rewrite (equiv_same_size t_eq_t'). apply size_direct_subterm; simpl; 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)