```
H : given_point a b (x :: t)
eq1 : nos = 0
IHimg' : given_point a b t -> false = true
```

Are these two hypothesises false?

What is `given_point`

, what is `nos`

?

given_point is function's name, nos a b :nat

If you manage to prove that ` given_point a b (x :: t) -> given_point a b t`

yes there is a contradiction, otherwise no

Last updated: Oct 04 2023 at 19:01 UTC