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?
This topic was moved to #Coq users > Coqhammer by Karl Palmskog.
Last updated: Nov 29 2023 at 21:01 UTC