Finished the 1st, 2nd and 3rd layers of the proof of lemma4 in charles' paper with the plan bound function symbol.