zohaze (May 01 2023 at 15:12): zohaze (May 01 2023 at 15:12):H : given_point a b (x :: t)
eq1 : nos = 0
IHimg' : given_point a b t -> false = true
Are these two hypothesises false?
Laurent Théry (May 01 2023 at 15:19):What is given_point, what is nos?
zohaze (May 02 2023 at 13:22):given_point is function's name, nos a b :nat
Laurent Théry (May 02 2023 at 14:04):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 13 2024 at 01:02 UTC