proposition: Lemma lt_roots : forall f g, g <F f -> forall ss ts, (forall t, In t ts -> lt t (Fun f ss)) -> lt (Fun g ts) (Fun f ss).
proof: Proof. intros f g ltgf ss ts Hsub. unfold lt; apply rpo1; trivial. Qed.
imports: CoLoR(VPrecedence MultisetListOrder ListLex VRPO_Type VTerm ListUtil AccUtil LogicUtil) Coq(Relations)