# How to check a Zenon-generated proof with Coq?

I installed zenon (opam package, github) and tried to use it to generate a Coq proof.

I couldn't find any documentation for the Zenon's main syntax, so I looked at its test suite.

I grabbed this test out of its test suite.

$$sig P ("nat") "Prop"$$sig Q ("nat") "Prop"

$$hyp "h1" (A. ((x "nat") (P x)))$$hyp "h2" (A. ((x "nat") (Q x)))
\$goal (-. (\/ (A. ((x "nat") (-. (Q x)))) (A. ((x "nat") (-. (P x))))))


zenon -ocoq test01.znn produces the following output.

(* PROOF-FOUND *)
(* BEGIN-PROOF *)
Theorem zenon_thm : (~((forall x : nat, (~(Q x)))\/(forall x : nat, (~(P x))))).
Proof.
apply NNPP. intro zenon_G.
apply zenon_G. zenon_intro zenon_H3.
apply (zenon_or_s _ _ zenon_H3); [ zenon_intro zenon_H5 | zenon_intro zenon_H4 ].
generalize (h2 O). zenon_intro zenon_H6.
generalize (zenon_H5 O). zenon_intro zenon_H7.
exact (zenon_H7 zenon_H6).
generalize (h1 O). zenon_intro zenon_H8.
generalize (zenon_H4 O). zenon_intro zenon_H9.
exact (zenon_H9 zenon_H8).
Qed.
(* END-PROOF *)


I wrote the above to test01.v and tried to compile that into a .vo file.

coqc test01.v
File "./test01.v", line 3, characters 43-44:

I'm not sure how to fix this. P and Q are both defined in the znn file.
zenon -v

coqc -v