Function f requires two arguments and gives true or false. When i apply destruct command then first case is being consider but it is not visible in hypothesis. I wan to see it in hypothesis. I have applied destruct f a b as eq1 so that it look like f a b=true first time (then f a b=false in hypothesis) but it does not work.
destruct (f a b) eqn:eq1.
Thank you for correction.
Last updated: Oct 04 2023 at 20:01 UTC