I have below statement in hypothesis

H: In S(S(S(S(S(S( a)))))) [2;3;4;5].

The natural number S(S(S(S(S(S( a)))))) will not exist in the list,for all vaues of a (0 or S a).

1) Could i prove above is wrong statement?

2) On the basis of this , H may i close any goal statement?

3) When simplify above, I get message " unknown a". How i can solve it?

1) Indeed the hypothesis `H`

implies `False`

.

2) Using `exfalso`

you can deduce any statement from a proof of `False`

.

Here is some corresponding Coq code:

```
From Coq Require Import List.
Import ListNotations.
Goal forall P a, In (S(S(S(S(S(S(a))))))) [2;3;4;5] -> P.
Proof.
intros P a H. exfalso.
repeat (destruct H; [ discriminate H | cbn in H ]).
exact H.
Qed.
```

thanks.

Last updated: Jun 20 2024 at 11:02 UTC