proposition: Lemma subterm_subterm_alt : forall t s, refl_trans_clos direct_subterm s t -> {p : list nat | subterm_at_pos t p = Some s}.
proof: Proof. assert (H : forall t s, refl_trans_clos direct_subterm s t -> exists p, subterm_at_pos t p = Some s). intros s t H; inversion H as [u | t' s' H']. subst; exists nil; apply eq_refl. subst s' t'; clear H; induction H' as [s t H | s t u H1 H2]. destruct t as [x | f l]. contradiction. simpl in H. destruct (in_split _ _ H) as [l1 [l2 H']]. exists (length l1 :: nil); subst l; simpl; rewrite nth_error_at_pos; apply eq_refl. destruct t as [x | f l]. contradiction. simpl in H1. destruct (in_split _ _ H1) as [l1 [l2 H']]. destruct IHH2 as [p Sub]; exists (p ++ (length l1) :: nil). apply subterm_in_subterm with (Term f l); trivial. subst l; simpl; rewrite nth_error_at_pos; apply eq_refl. intros t s H'; destruct (subterm_at_pos_dec t s) as [Sub | not_Sub]. assumption. apply False_rect. destruct (H _ _ H') as [p Sub]; apply (not_Sub p Sub). Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)