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