fact: Definition size_direct_subterm : forall t1 t2, direct_subterm t1 t2 -> size t1 < size t2.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)