
Robbert Krebbers authored
It does not really help since the main work of the proof is in showing that `cFunctor_map F (iProp_fold, iProp_unfold)` is injective, but whatever.
ec0816bf
It does not really help since the main work of the proof is in showing that `cFunctor_map F (iProp_fold, iProp_unfold)` is injective, but whatever.