3 ms·

I don't think it's that easy. Not every statement is either true or false in Coq, you'd need to accept the law of excluded middle for that.