proposition: Lemma is_subterm_ok_true : forall s t, is_subterm s t = true -> {p : list nat | subterm_at_pos t p = Some s}.
proof: Proof. intros s t; pattern t; apply term_rec3; clear t. destruct s as [y | ]; simpl; intros x H; [ | discriminate]. exists nil; simpl; do 2 apply f_equal; generalize (X.eq_bool_ok x y); rewrite H; exact (fun H => H). destruct s as [x | g k]; intros f l IHl H. revert IHl H. induction l as [ | t l IHl0]; intros IHl H. discriminate. case_eq (is_subterm (Var x) t). intro Sub; destruct (IHl _ (or_introl _ (eq_refl _)) Sub) as [p Sub']. exists (0 :: p); assumption. intro nSub; simpl in H; rewrite nSub in H; destruct IHl0 as [p Sub]. intros; apply IHl; [right | ]; assumption. assumption. destruct p as [ | i p]. discriminate. exists (S i :: p); simpl; assumption. case_eq (eq_bool (Term f l) (Term g k)). intro s_eq_t; exists nil. generalize (eq_bool_ok (Term f l) (Term g k)); rewrite s_eq_t; intro s_eq_t'; simpl; apply f_equal; assumption. intro s_diff_t; generalize (eq_bool_ok (Term f l) (Term g k)); rewrite s_diff_t. simpl in H; simpl in s_diff_t; rewrite s_diff_t in H; simpl in H. clear s_diff_t; intros _. assert (H' : {i : nat & {p : list nat | subterm_at_pos (Term f l) (i :: p) = Some (Term g k)}}). simpl; revert IHl H; induction l as [ | t l IHl0]; intros IHl H. discriminate. case_eq (is_subterm (Term g k) t). intro Sub; destruct (IHl _ (or_introl _ (eq_refl _)) Sub) as [p Sub']. exists 0; exists p; assumption. intro nSub; simpl in H; rewrite nSub in H. destruct IHl0 as [i [p Sub]]. intros; apply IHl; [right | ]; assumption. assumption. exists (S i); exists p; simpl; assumption. destruct H' as [i [p Sub]]; exists (i :: p); assumption. Defined.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)