minor (rename rules)
completed proof of 1st NI lemma