Argument to bi_pure should have argument at type_scope?
The argument of
bi_pure is marked as
stdpp scope, which seems odd since it is a
Prop? This works since all notations inside of stdpp have stdpp_scope, but it isn't nicely compatible with non stdpp notations.
If you already have a
Open Scope stdpp_scope in your file, you should already get access to notations in stdpp scope.