Lsharp in Coq