Add lemmas for using `IdFree` at the logic level.

This MR adds analogues of id_freeN_r and id_freeN_l at the logic level. Needed for !930 (closed).