```
H1 : f4 a b 0 [] = true
Fixpoint f4 (a b c : nat) ( l : list nat) : bool :=
match c with
|0=> false
|S n=> match l with
|nil =>false
|h::t=>...
```

f4 gives false in case c=0 & l=[]. But i have hypothesis that it gives true . I want to write left side of f4=false so that

it become false=true. I simply unfold f4 then

get message fix f4

(a b c : nat) (l : list nat) : bool :=

match c with

|0=>false

|S _=>

Why this happening when i already destruct c?

Last updated: Jun 25 2024 at 15:02 UTC