proposition: Lemma immediate_subterm_property : forall s f ss, In s ss -> lt s (Fun f ss).
proof: Proof. intros s f ss Hin. apply lt_subterm. exists s. split; try left; trivial. Qed.
imports: CoLoR(VRPO_Type VTerm Preorder ListUtil RelUtil LogicUtil AccUtil) Coq(Peano_dec)