proposition: Lemma subterm_subterm : forall t p s, subterm_at_pos t p = Some s -> (t=s) \/ (trans_clos direct_subterm s t).
proof: Proof. intros t p; generalize t; clear t; induction p as [ | i p]; intros t s Sub; simpl in Sub. injection Sub; intros; subst; left; trivial. destruct t as [v | f l]. discriminate. right; assert (H := nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]. destruct (H _ (eq_refl _)) as [l1 [l2 [L H']]]. destruct (IHp _ _ Sub) as [ti_eq_s | Subi]. subst; apply t_step; simpl; apply in_or_app; right; left; trivial. apply trans_clos_is_trans with ti; trivial. subst; apply t_step; simpl; apply in_or_app; right; left; trivial. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)