Module Fset should be ghost
Either that or it should be monomorphic with respect to equality. Indeed, as it stands, the following program is verifiable:
use set.Fset
type t = { ghost b : bool }
let f ()
ensures { result = 2 }
=
let s = singleton { b = false } in
let s = add { b = true } s in
cardinal s