Output of (f a b) is bool.When i apply destruct command on if (f a b) then Coq consider it true and then false with

no hypothesis . What command i should apply that in hypothesis it appears as (f a b) =true and

next (f a b) =false also.

`destruct (f a b) eqn:Heq`

will give you `Heq : f a b = true`

or `= false`

additionally.

thanks

Last updated: Jun 15 2024 at 08:01 UTC