```
H: true &&
match t with
| [] => false
| b :: t =>
if f b c
then
determin z1 z2 n l b t
(fur q s values)
else false
end = true
goal: true &&
(if f b c
then
determin z1 z2 n l b t
(fur q s values)
else false) = true
```

I have hypothesis and goal more or less in same form. How i can use H in solving goal statement? In present situation first command i should apply is induction t in H (am i right?)

If i do this , then induction t as [ | b' t1].

```
H1: determin z1 z2 n l b' t1
(fur q s values)= true
goal: determin z1 z2 n l b tl'
(fur q s values)= true
```

still i can't use H1. How to come out?

in `H`

, the first `t`

is shadowed by its tail. So these assumptions really mean something different.

I have simplified/modified above . Output of fur (value s k (d:: l)) is list nat. q s c are nat.

H:=In c l

goal: match fur (value s q (d:: l)) with

| [] => false

Now again this is false due to the occurence of d & c. I have applied destruct command on fur (value s k (d:: l)) then get false=true. To avoid this i should have inversion . May i write it as In c l -> In c [] -> False. When i will apply it then from where i bring In c [] . (or some other way)

Maybe you need to keed track of the value of `fur`

to finish the proof

```
destruct (fur (value s q (d :: l))) as [|x xl] eqn : Heq.
```

Last updated: Jun 23 2024 at 23:01 UTC