proposition: Lemma strict_subterm_less : forall s f ss, In s ss -> lt_mpo s (Fun f ss).
proof: Proof. intros s f ss Hin. constructor 3. exists s. split; try left; trivial. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)