WIP: Make `[#]` produce goal with `<pers>` modality if premise is not persistent

This is my attempt at working towards #186

Currently the iAssert has not been fixed yet, but I would like to see if I am at least going in the right direction. With the modifications you can now use iSpecialize with on persistent hypothesis to produce a persistent result. E.g. the following works:

Lemma test_specialize `{BiBUpd PROP} (P Q : PROP) :
  □ P -∗ □ (P -∗ Q) -∗ □ Q.
Proof.
  iIntros "#HP #H".
  iSpecialize ("H" with "[#]").
  { iIntros "!>". iAssumption. }
  iAssumption.
Qed.

The following works as well:

Lemma test_specialize_2 `{BiBUpd PROP} (P Q : PROP) :
  □ P -∗ □ (□ P -∗ Q) -∗ □ Q.
Proof.
  iIntros "#HP #H".
  iSpecialize ("H" with "[#]").
  { iIntros "!>". iAssumption. }
  iAssumption.
Qed.