proposition: Lemma subterm_in_instantiated_term : forall p s t sigma, subterm_at_pos (apply_subst sigma t) p = Some s -> match subterm_at_pos t p with | Some u' => s = apply_subst sigma u' | None => exists v, exists q, exists q', p = q ++ q' /\ In v (var_list t) /\ subterm_at_pos t q = Some (Var v) /\ subterm_at_pos (apply_subst sigma (Var v)) q' = Some s end.
proof: Proof. intro p; induction p as [ | i p]; intros s t sigma Sub. simpl in Sub; injection Sub; clear Sub; intros; subst; simpl; trivial. simpl; simpl in Sub; destruct t as [v | f l]. exists v. simpl in Sub; destruct (find eq_var_bool v sigma) as [v_sigma | ]. exists (@nil nat); exists (i :: p); repeat split; trivial. left; trivial. discriminate. simpl in Sub. assert (H := nth_error_map (apply_subst sigma) l i). destruct (nth_error (map (apply_subst sigma) l) i) as [ti_sigma | ]. assert (H' := nth_error_ok_in i l). destruct (nth_error l i) as [ti | ]. destruct (H' _ (eq_refl _)) as [l1 [l2 [L H''']]]; clear H'; subst; generalize (IHp _ _ _ Sub). destruct (subterm_at_pos ti p) as [u | ]; trivial. intros [v [q [q' [p_eq_qq' [v_in_ti [Sub' Sub'']]]]]]. exists v; exists (length l1 :: q); exists q'; repeat split; trivial. subst p; trivial. apply var_in_subterm with ti (length l1 :: nil); trivial. simpl; rewrite nth_error_at_pos; trivial. simpl; rewrite nth_error_at_pos; trivial. contradiction. discriminate. Qed.
imports: Coq(Recdef List Arith Setoid) CoLoR(closure more_list list_permut list_set decidable_set term_spec) CoLoR.Util.Nat(NatCompat)