Jh/validity
"Validity" coercion from iProp to Prop. Magic wand that works at the Prop level.
The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.
"Validity" coercion from iProp to Prop. Magic wand that works at the Prop level.
The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.