[clarus]

It shoud be possible. A specific feature of Coq that we use is impredicative Set. I do not know if this is the case in F*.