Turn Coq quantifiers into proofmode quantifiers on `iStartProof`
For example, it should turn the Coq goal
forall x, P ⊢ Q into a proof mode goal
∀ x, P → Q. (And likewise for let-bindings).
Since issue came up in d7db5250, which changes the behavior of
iStartProof PROP, to just introduce all quantifiers. @jjourdan introduced that because in iGPS they were often doing:
intros; iStartProof (uPred _); iIntros (V) "..."
The proposal in this issue fixes this problem in a nicer way.