Skip to content

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

Ike Mulder requested to merge snyke7/iris:ike/id_free_internal into master

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

Merge request reports

Loading