Trials to finish The lemmas about replace_projected()
This is the current progress before proving bound_child_parent_lemma_1_1_1_3_1