proposition: Lemma subterm_at_pos_dec : forall t s, {p : list nat | subterm_at_pos t p = Some s}+{forall p, subterm_at_pos t p <> Some s}.
proof: Proof. fix subterm_at_pos_dec 1. intros t; case t; clear t. intros x s; case s; clear s; [intro x'| intros f' l']. generalize (X.eq_bool_ok x x'); case (eq_var_bool x x'). intro x_eq_x'; left; exists nil; rewrite x_eq_x'; reflexivity. intro x_diff_x'; right; intros p; case p; clear p. intro H; apply x_diff_x'; injection H; clear H; intro H; exact H. intros n p H; discriminate. right; intros p; case p; clear p. intro H; discriminate. intros n p H; discriminate. intros f l s; generalize (eq_bool_ok (Term f l) s); case (eq_bool (Term f l) s). intro t_eq_s; left; exists nil; rewrite <- t_eq_s; reflexivity. intros t_diff_s; assert (IH : forall t, In t l -> forall s, {p : list nat | subterm_at_pos t p = Some s} + {(forall p : list nat, subterm_at_pos t p <> Some s)}). clear - subterm_at_pos_dec. revert l; fix subterm_at_pos_dec_list 1. intro l; case l; clear l. intros t Abs; elim Abs. intros t1 l t t_in_t1l; generalize (eq_bool_ok t t1); case (eq_bool t t1). intros t_eq_t1 s; rewrite t_eq_t1; apply subterm_at_pos_dec. intros t_diff_t1 s; apply (subterm_at_pos_dec_list l t). simpl in t_in_t1l; case t_in_t1l; clear t_in_t1l. intro t1_eq_t; apply False_rect; apply t_diff_t1; rewrite t1_eq_t; reflexivity. intro t_in_l; exact t_in_l. assert (IH' : forall s, {n :nat & {t : term & {p | (nth_error l n) = Some t /\ subterm_at_pos t p = Some s}}} + {(forall t, In t l -> forall p, subterm_at_pos t p <> Some s)}). clear -IH. revert l IH; fix subterm_at_pos_dec 1. intro l; case l; clear l. intros _ s; right; intros t Abs; elim Abs. intros t l IH s. case (IH t (or_introl _ (eq_refl _)) s). intro s_in_t; case s_in_t; intros p Sub; left; exists 0; exists t; exists p; split. reflexivity. assumption. intro s_not_in_t; case (subterm_at_pos_dec l (tail_set _ IH) s). intro s_in_l; case s_in_l; intros n H; case H; clear H; intros tn H; case H; clear H; intros p H; case H; clear H; intros E Sub. left; exists (S n); exists tn; exists p; split; assumption. intro s_not_in_l; right. intros t' t'_in_tl; simpl in t'_in_tl; case t'_in_tl. intro t_eq_t'; rewrite <- t_eq_t'; exact s_not_in_t. exact (s_not_in_l t'). case (IH' s); intro H. case H; clear H; intros n H; case H; clear H; intros t H; case H; clear H; intros p H; case H; clear H; intros E Sub. left; exists (n :: p); simpl; rewrite E; assumption. right; intro p; case p; clear p. simpl; intro t_eq_s; apply t_diff_s; injection t_eq_s; intro t_eq_s'; exact t_eq_s'. intros n p; simpl. generalize (nth_error_ok_in n l); case (nth_error l n). intros tn H'; case (H' tn (eq_refl _)); clear H'. intros l1 H'; case H'; clear H'. intros l2 H'; case H'; clear H'. intros L H'. apply (H tn); rewrite H'; apply in_or_app; right; left; reflexivity. intros _; discriminate. Defined.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)