Anyone good at Coq? Need someone to work on some proofs