`iStartProof` does not preserve names of quantified variables
Lemma test_iStartProof_variable_names (Φ: nat → PROP) :
∀ y, Φ y -∗ ∃ x, Φ x.
Proof. iStartProof.
Now the goal is ∀ x : nat, Φ x -∗ ∃ x0 : nat, Φ x0
: iStartProof
does not preserve the name y
properly.