```
a = c \/ False ->
a = d \/ False ->
g_value x y z (a::l1)=true
```

First , what is the meaning of above?

Secondly, I have two functions whose input arguments are (nat &list nat) and output is bool.Both functions gives true only when list length is greater than 3. To write lemma statement i should add constraint of length>3?

You should be able to prove `c = d \/ False`

equivalent to `c = d`

.

Could you upload a paste of your file to get an understanding what you're trying to do?

I have simplified above . Now this is the case where one constructor give following

```
Fixpoint g (x y z: nat) ( l : list nat) : bool :=
match z with
|0=> false
|S n' => match l with
| nil => false
| [a] =>if (eqb x y && eqb x a) then true else false
...
```

g x y (S z) [a] = true ->

eqb x y =true. To prove this I should apply induction so that discuss cases one by one. When i simplify g i get match g with o |Sn'. Although i have ( S z) in hypothesis. Now what to do?

This should work:

```
Goal forall x y z a, g x y (S z) [a] = true -> eqb x y = true.
intros x y z a; simpl; case (eqb x y); [trivial | discriminate].
Qed.
```

You sent an incomplete definition of `g`

(using `...`

dots). I don't think it's up to us to guess missing parts of code.

Last updated: Jun 14 2024 at 18:01 UTC