This happened for example in <[i:=x]>∅, where simpl unfold insert (despite it being declared simpl never) because ∅ reduces to a constructor.
