Patrick Nicodemus (Apr 16 2023 at 15:56): Patrick Nicodemus (Apr 16 2023 at 15:56):I tried to prove this with Coqhammer:
Theorem abc2 : exists k : nat * nat, fst k = 0 /\ snd k = 3
and it failed. I am wondering what the problem is here, is it with the use of product types?
Notification Bot (Apr 16 2023 at 17:28):This topic was moved to #Coq users > Coqhammer by Karl Palmskog.
Last updated: Nov 29 2023 at 21:01 UTC