proposition: Lemma size_direct_subterm : forall t1 t2, direct_subterm t1 t2 -> size t1 < size t2.
proof: Proof. intros t1 t2; unfold direct_subterm; destruct t2 as [ x | f l ]. contradiction. rewrite (size_unfold (Term f l)). induction l as [ | t l]; simpl; intuition. subst; auto with arith. apply Nat.lt_le_trans with (1 + list_size size l); trivial; simpl; auto with arith. Qed.
imports: Coq(List Arith) hydras(more_list list_permut list_set)