Proofs starting with <+> have level 0, not level 1

[ahelwer]

This should parse correctly:

(* ID: ImmediatePlusProof *)
LEMMA ImmediatePlusProof == RefersTo(v, "v")'
<+> RefersTo(c, "c")
(* ID: ImmediatePlusProof!<0>a *) <0>a RefersTo(v, "v")
<0> QED BY RefersTo(<0>a, "ImmediatePlusProof!<0>a")

Instead, the grammar will expect the level to be 1:

(* ID: ImmediatePlusProof *)
LEMMA ImmediatePlusProof == RefersTo(v, "v")'
<+> RefersTo(c, "c")
(* ID: ImmediatePlusProof!<1>a *) <1>a RefersTo(v, "v")
<1> QED BY RefersTo(<1>a, "ImmediatePlusProof!<1>a")

[ahelwer]

This could possibly be because last_proof_level is not being cleared when a proof finally ends.