proposition: Lemma subterm_subterm_non_nil : forall t p s, subterm_at_pos t p = Some s -> p <> nil -> (trans_clos direct_subterm s t).
proof: Proof. intros t p s H H0. generalize (subterm_subterm t p H). destruct 1;[|assumption]. subst. destruct p. elim H0;reflexivity. generalize (size_subterm_at_pos s n p). rewrite H. intros h;apply False_ind;apply (Nat.lt_irrefl _ h). Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)