proposition: Lemma rpo_subterm_mem : forall bb s f l, rpo bb (Term f l) s -> forall tj, mem equiv tj l -> rpo bb tj s.
proof: Proof. intros bb s f l fl_lt_s tj tj_mem_l. destruct (mem_split_set _ _ equiv_bool_ok _ _ tj_mem_l) as [tj' [l1 [l2 [tj_eq_tj' [H _]]]]]. simpl in tj_eq_tj'; simpl in H. rewrite (equiv_rpo_equiv_2 _ tj_eq_tj'). apply rpo_subterm with (Term f l); trivial. subst l; 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)