proposition: Lemma rpo_subterm : forall bb s t, rpo bb t s -> forall tj, direct_subterm tj t -> rpo bb tj s.
proof: Proof. intros bb s t; cut (forall p : term * term, match p with | (s,t) => rpo bb t s -> forall tj, direct_subterm tj t -> rpo bb tj s end). intro H; apply (H (s,t)). clear s t; intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s [ v | f l]] IH t_lt_s tj tj_in_l; simpl in tj_in_l; [ contradiction | idtac]. inversion t_lt_s as [ f' l' t' s' s'_in_l' t'_le_s' | f' g' k k' g'_prec_f' H | f' g k k' Sf' Sg f_eq_g L k'_lt_k H | f' g k k' Sf' Sg f_eq_g k'_lt_k ]. subst; inversion t'_le_s' as [ t'' s'' t'_eq_s' | t'' s'' t'_lt_s']; clear t'_le_s'; subst. apply (@Subterm bb f' l' tj s'); trivial; apply Lt; apply rpo_subterm_equiv with (Term f l); trivial. apply (@Subterm bb f' l' tj s'); trivial. apply Lt; apply (IH (s', Term f l)); trivial. apply size2_lex1_mem; trivial. subst; apply H; apply in_impl_mem; trivial. intros; apply Eq. subst; apply H; apply in_impl_mem; trivial. intros; apply Eq. inversion k'_lt_k as [a lg ls lc l1 l2 P1 P2 H']; subst. assert (tj_mem_l := in_impl_mem equiv Eq tj l tj_in_l). rewrite (mem_permut0_mem equiv_equiv tj P1) in tj_mem_l. rewrite <- mem_or_app in tj_mem_l. destruct tj_mem_l as [tj_mem_ls | tj_mem_llc]. destruct (H' _ tj_mem_ls) as [a' [a'_mem_a_lg tj_lt_a']]. apply (@Subterm bb g k tj a'). rewrite (mem_permut0_mem equiv_equiv a' P2); rewrite app_comm_cons. rewrite <- mem_or_app; left; trivial. apply Lt; trivial. apply (@Subterm bb g k tj tj). rewrite (mem_permut0_mem equiv_equiv tj P2). right; rewrite <- mem_or_app; right; trivial. apply Equiv; apply Eq. 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)