Skip to content

Prove sigT_equivI is admissible (fix #250)

Paolo G. Giarrusso requested to merge Blaisorblade/iris:sigT_equivI-admissible into master

I think this is all that's needed, right? I've already used this statement (with the iProp-only proof) to simplify the ugly proofs @robbertkrebbers saw today — and this adds no obligation on the interface.

Merge request reports