proposition: Lemma subterm_at_pos_apply_subst_apply_subst_subterm_at_pos : forall t p sigma, match subterm_at_pos t p with | Some u => subterm_at_pos (apply_subst sigma t) p = Some (apply_subst sigma u) | None => True end.
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v p; destruct p as [ | i q ]; simpl; trivial. intros f l IHl p; destruct p as [ | i q ]; simpl; trivial. assert (H : forall (l : list term) i, match nth_error l i with | Some li => In li l | None => True end). clear IHl l i; intro l; induction l as [ | t l ]; intro i; destruct i as [ | i ]; simpl; trivial. left; trivial. generalize (IHl i); destruct (nth_error l i); trivial; intros; right; trivial. generalize i; clear i; induction l as [ | l ll ]; intros i; destruct i as [ | i ]; simpl; trivial. intros; apply IHl; left; trivial. intro sigma; apply IHll; intros; apply IHl; right; trivial. Qed.
imports: List more_list list_permut list_set Arith