coding style adjustments in prosa.util.exists_extensionality
I've edited your addition in prosa.util to highlight some ways in which I'd like you to adhere more to the Prosa coding style:
-
Use coqdoc comments before any top-level item.
-
Introduce context (types, hypothesis, variables) with comments as section variables.
-
Either use structured sub-proofs (bullet points or curly braces) or dispatch in one go with chained
;. -
Use P and Q as "standard" names for predicates. (This one isn't so important. Just cosmetics.)
Let me know if you have any questions.