fof(emptyset_in_unit,conjecture,elem(emptyset,unit)).
fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))).
fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))).