Definition. We define False to be ∀p : prop, p of type prop.

In Proofgold the corresponding term root is 1db705... and object id is 266ad5...

Axiom. (setnonempty) We take the following as an axiom:

∀p : prop, (∀x : set, p) → p

In Proofgold the corresponding term root is 938253... and proposition id is dcb328...