How to check a Zenon-generated proof with Coq?

Question

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:
Error: The reference Q was not found in the current environment.

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

Here are the versions of Coq and Zenon involved:

zenon -v
zenon version 0.8.5 [a270] 2020-10-23

coqc -v
The Coq Proof Assistant, version 8.16.1
compiled with OCaml 4.11.1