show a stronger lemma-checkInsert-restrict