Skip to content

prove general fmap_inj lemmas

Ralf Jung requested to merge ralf/fmap_inj into master

and derive the existing ones from it (and also in Iris, an equivalent one for dist)

Merge request reports