{"action":"created","issue":{"url":"https://api.github.com/repos/snu-sf/pl2015/issues/112","labels_url":"https://api.github.com/repos/snu-sf/pl2015/issues/112/labels{/name}","comments_url":"https://api.github.com/repos/snu-sf/pl2015/issues/112/comments","events_url":"https://api.github.com/repos/snu-sf/pl2015/issues/112/events","html_url":"https://github.com/snu-sf/pl2015/issues/112","id":78353030,"number":112,"title":"BEq a a0 = true or false","user":{"login":"HyeongMee","id":8803802,"avatar_url":"https://avatars.githubusercontent.com/u/8803802?v=3","gravatar_id":"","url":"https://api.github.com/users/HyeongMee","html_url":"https://github.com/HyeongMee","followers_url":"https://api.github.com/users/HyeongMee/followers","following_url":"https://api.github.com/users/HyeongMee/following{/other_user}","gists_url":"https://api.github.com/users/HyeongMee/gists{/gist_id}","starred_url":"https://api.github.com/users/HyeongMee/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/HyeongMee/subscriptions","organizations_url":"https://api.github.com/users/HyeongMee/orgs","repos_url":"https://api.github.com/users/HyeongMee/repos","events_url":"https://api.github.com/users/HyeongMee/events{/privacy}","received_events_url":"https://api.github.com/users/HyeongMee/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-05-20T03:35:33Z","updated_at":"2015-05-20T04:39:30Z","closed_at":null,"body":"How can I express \"BEq a a0 is either true or false\" in Coq? \r\nThere's nothing like BOr;; So I am stuck in the 4th problemTT"},"comment":{"url":"https://api.github.com/repos/snu-sf/pl2015/issues/comments/103751751","html_url":"https://github.com/snu-sf/pl2015/issues/112#issuecomment-103751751","issue_url":"https://api.github.com/repos/snu-sf/pl2015/issues/112","id":103751751,"user":{"login":"jaewooklee93","id":11328376,"avatar_url":"https://avatars.githubusercontent.com/u/11328376?v=3","gravatar_id":"","url":"https://api.github.com/users/jaewooklee93","html_url":"https://github.com/jaewooklee93","followers_url":"https://api.github.com/users/jaewooklee93/followers","following_url":"https://api.github.com/users/jaewooklee93/following{/other_user}","gists_url":"https://api.github.com/users/jaewooklee93/gists{/gist_id}","starred_url":"https://api.github.com/users/jaewooklee93/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaewooklee93/subscriptions","organizations_url":"https://api.github.com/users/jaewooklee93/orgs","repos_url":"https://api.github.com/users/jaewooklee93/repos","events_url":"https://api.github.com/users/jaewooklee93/events{/privacy}","received_events_url":"https://api.github.com/users/jaewooklee93/received_events","type":"User","site_admin":false},"created_at":"2015-05-20T04:39:30Z","updated_at":"2015-05-20T04:39:30Z","body":"Do you want to perform a case analysis on that? Then you may be able to use ```destruct eqn``` like below.\r\n\r\n```Coq\r\ndestruct (beval st (BEq a a0)) eqn:B.\r\n```\r\n\r\nThen the goal will be separated into two cases, namely ```(BEq a a0=true)``` and ```(BEq a a0=false)```. However, I definitely believe that you don't need to write code in this way to solve 4th one."}}