Skip to content

add lemmas for core of auth⋅frag in view and auth

Ralf Jung requested to merge jung/iris:view-both-core into master

Leftovers from my first approach to !827 (merged), that I think might still be useful.

Merge request reports