proposition: Lemma replace_at_pos_is_replace_at_pos2 : forall t p u, subterm_at_pos t p = Some u -> replace_at_pos t u p = t.
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v p u; destruct p as [ | i q ]; intro H; inversion_clear H; trivial. intros f l IHl p; destruct p as [ | i q ]. intros u H; inversion_clear H; trivial. intros u H; rewrite replace_at_pos_unfold; apply (f_equal (fun l => Term f l)); generalize i q u H; clear i q u H; induction l as [ | t l ]; intros i q u H. destruct i as [ | i ]; simpl; intros; discriminate. destruct i as [ | i ]; simpl. rewrite IHl; trivial; left; trivial. rewrite IHl0; trivial; intros; apply IHl; trivial; right; trivial. Qed.
imports: List more_list list_permut list_set Arith