proposition: Lemma replace_at_pos_list_replace_at_pos_in_subterm : forall l1 ui l2 u i p, length l1 = i -> replace_at_pos_list (l1 ++ ui :: l2) u i p = l1 ++ (replace_at_pos ui u p) :: l2.
proof: Proof. intros l1; induction l1 as [ | u1 l1 ]; intros ui l2 u i p L; simpl in L. subst i; trivial. destruct i as [ | i ]. discriminate. simpl; rewrite IHl1; trivial. inversion L; trivial. Qed.
imports: List more_list list_permut list_set Arith