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:

1. Use coqdoc comments before any top-level item.

2. Introduce context (types, hypothesis, variables) with comments as section variables.

3. Either use structured sub-proofs (bullet points or curly braces) or dispatch in one go with chained ;.

4. 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.

closed