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