set(auto2). formulas(sos). % axioms for theorem 1b (uniqueness) all x all G ((Object(x) & Property(G)) -> (IsAFormOf(x,G) <-> (Ex1(A,x,W) & (all F (Property(F) -> (Enc(x,F) <-> Implies(G,F))))))). all x all G (IsAFormOf(x,G) -> Object(x) & Property(G)). all x all y ((Object(x) & Object(y) & Ex1(A,x,W) & Ex1(A,y,W)) -> ((all F (Property(F) -> (Enc(x,F) <-> Enc(y,F)))) -> x = y)). end_of_list.