"git-rts@gitlab.mpi-sws.org:proux/iris.git" did not exist on "b2bb853ffd1ac0c92cf28636f9dee80a92c50cb3"
Include fragment in `mnat_auth_auth`.
This gives the following new lemma: ```coq Lemma mnat_auth_included q n : mnat_auth_frag n ≼ mnat_auth_auth q n. ``` Also reorganize the files slightly so that validity lemmas are grouped together.
parent
59c3f672
No related branches found
No related tags found
Please register or sign in to comment