```
H2: match value d [y] with
| []=>false
|b::l=>....
```

First case is false due to the occurence of y in list. To simplify H2 , i should apply induction on [y]. Or un fold vaue function in H2 to show and prove that this function gives false only in case of empty input list. One element of list is y,If i need information of second elements of same list then i have to apply induction again or simply apply destruct? What is the simplest way of simplify above?

Hi, the answer depends completely on the definition of `value`

. This is precisely why we ask to always give a completely compilable code snippet. If value is a fixpoint decreasing on its second argument, then probably unfold is the way to try, if not, well, I need more.

Last updated: Jun 14 2024 at 20:01 UTC