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.

Syntax is `destruct (f a b) eqn:eq1`

.

Thank you for correction.

Last updated: Oct 04 2023 at 20:01 UTC