Fill in the FSetInterface implementations and proof obligations
Fill in the FSetInterface implementations and proof obligations

For the implementations, we can make good use of `Program Fixpoint`. The
proofs are still somewhat tedious; maybe someone can come up with the
right tactics here.

antalsz/hs-to-coq,antalsz/hs-to-coq