```
H: chk r1 r2 (k1 :: k2 :: t)=true
H1: r1=k1
H2: r2=k2
IH3: k2::t<>[] ->
chk r1 r2 (k2:: t)=true->
In r1(k2:: t)->
In r2(k2:: t)->
f3 r2(k2:: t)=true->
f4 r2(k2:: t)=true.
```

Co-existence of above 4 hypothesis is false because H1(r1=k1) & In r1(k2:: t).How i could prove it false?

Plz, some one help me in proving H1 & IH3 are contra statement?

we don´t know was `f3`

`f4`

`chk`

are. How can we help you....

We asked several times for snippets in Coq we could download and replay, not trying to guess missing information.

Yes, you have pointed out many times. But i have represented the functions by f1,f2..just to keep code simple. Secondly,

H1: r1=k1 & In r1(k2:: t) [in IH3] are not possible at a time (point of contradiction is clear here). Third whatever f3 & f4 it gives true on the basis of wrong assumption.Therefore it results in true=false. If i am wrong then just give comment on H1: r1=k1 & In r1(k2:: t) [in IH3] or how these f2 f3 play their role ? Thank u.

The fact that `In r1 (k2 :: t)`

is not possible in `IH3`

simply says that `iH3`

is of the form `False -> ..`

. So `IH3`

is no contradictory, it just means `IH3`

is useless : we cannot derive anything from it.

ok.

Last updated: Oct 04 2023 at 21:01 UTC