Wrong placement of braces

[qbuzet]

require open Blanqui.Lib.Set Blanqui.Lib.Prop  Blanqui.Lib.Eq Blanqui.Lib.Bool;

symbol istrue : 𝔹 → Prop;

rule istrue true ↪ ⊤
with istrue false ↪ ⊥;

symbol b : π(true ≠ false) ≔
begin
  assume h;
  have f: π (istrue false) {
    rewrite left h; refine top; };
  refine ⊥ₑ _ f ;
end;

symbol b : π(true ≠ false) ≔
begin
  assume h;
  have f: π (istrue false) {
    rewrite left h; refine top;
  refine ⊥ₑ _ f ; };
end;

We can do both indifferently but the goal of "have" is proved when applying "refine top". Braces are well required but there is no mechanism to detect the end of a sub-proof. It seems this bug works with other tactics like induction, apply...