proposition: Lemma rpo_subterm : forall s t, rpo t s -> forall tj, direct_subterm tj t -> rpo tj s.
proof: Proof. intros s t; cut (forall p : term * term, match p with | (s,t) => rpo t s -> forall tj, direct_subterm tj t -> rpo tj s end). intros H; apply (H (s,t)). clear s t; intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p; intro p; destruct p; rename t into s; rename t0 into t; intros IH H tj In_tj; inversion H; clear H. subst s t0; inversion H1; clear H1. subst s0 t0; apply (Subterm f l tj t); trivial; apply Lt; destruct t; try contradiction; apply (Subterm s l0 tj tj); trivial; apply Eq; trivial. subst t t0; apply (Subterm f l tj s0); trivial; apply Lt; refine (IH (s0, s) _ _ tj _); trivial. unfold o_size2, size2, lex; elim (eq_nat_dec (size s0) (size (Term f l))); intro eq1. absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm s0 (Term f l) H0); rewrite eq1; trivial. apply size_direct_subterm; trivial. subst t s; apply H1; trivial. subst t s; apply H2; trivial. subst t s; inversion H1; clear H1. subst l'0 l0; simpl in In_tj; elim (in_app_or _ _ _ (in_permut_in tj In_tj H)); clear In_tj; intro In_tj. elim (H3 tj In_tj); intros a' H4; elim H4; clear H4; intros H4 H5. apply (Subterm f l tj a'); [ refine (in_permut_in a' _ (list_permut_sym H2)); rewrite app_comm_cons; apply in_or_app; left | apply Lt; apply H5 ]; trivial. apply (Subterm f l tj tj); [ refine (in_permut_in tj _ (list_permut_sym H2)); right; apply in_or_app; right | apply Eq ]; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term