proposition: Lemma rpo_subterm_equiv : forall bb s t, equiv t s -> forall tj, direct_subterm tj t -> rpo bb tj s.
proof: Proof. intros bb s [ | f l] fl_eq_s tj; simpl. contradiction. intro tj_in_l; rewrite <- (equiv_rpo_equiv_1 _ fl_eq_s). apply Subterm with tj. apply in_impl_mem; trivial. intros; apply Eq. intros; 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)