prove the remaining parts of lemma-checkInsert-generate