>>217
はっきり見てないけど、こことか参考にならないかな？
https://stackoverflow.com/questions/16555022/proving-if-then-else-in-coq