Simplification in imset2 should be locked

[hivert]

Consider the following code:

Variable (f1 f2 : {fset nat}).
Lemma bla : [fset (n1 + n2)%N | n1 in f1, n2 in f2] == fset0.
Proof.
rewrite /=.

Then the goal is:

  f1, f2 : {fset nat}
  ============================
  Imfset.imfset2 imfset_key (K:=nat_choiceType) (T1:=nat_choiceType)
    (T2:=fun _ : nat => nat_choiceType) (fun n1 : nat => [eta addn n1])
    (p1:=mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) f1))
    (p2:=fun _ : nat =>
         mem_fin (fin_finpred (pT:=fset_finpredType nat_choiceType) f2))
    (Phantom (mem_pred nat) (mem f1))
    (Phantom (nat -> mem_pred nat) (fun _ : nat => mem f2)) == fset0

Which is completely unreadable. I think the simplification should not be possible except after some form of unlocking.

[CohenCyril]

This looks more like a notation not printing correctly bug than a simplification problem... I will investigate the problem.