proposition: Lemma trans_clos_subterm_rpo: forall bb s t, (trans_clos direct_subterm) s t -> rpo bb s t.
proof: Proof. intros bb s t H; induction H as [ s [ v | f l ] H | s t u H1 H2]. inversion H. apply (@Subterm bb f l s s); trivial. simpl in H; apply in_impl_mem; trivial. exact Eq. apply Equiv; apply Eq. apply (@rpo_subterm bb u t); 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)