problem-set/algebra/category.theory/p16.desc created : 07/05/89 revised : 07/07/89 Natural Language Description: Lemma 16 : If x exists, then dom(x) exists. Versions : p16.ver1 : in Mitchell's axiom system, this cannot be expressed. p16.ver2 : in Quaife's axiom system, this cannot be expressed. p16.ver3 : Scott axioms, using UR resolution. created : from Scott, "Identity & Existence in Intuitionist Logic" [1978]. verified for ITP : Untested. translated for OTTER by : caw. verified for OTTER : 07/07/89.