I have a Q: val -> iProp, now I want to save predicate Q just like the saved proposition. How to do that?
Q: val -> iProp
Q