proposition: Lemma powerAx X Y : ele Y (power X) <-> sub Y X.
proof: Proof. destruct (classof_ex Y) as [t ->]. destruct (classof_ex X) as [s ->]. rewrite power_welldef, classof_ele, classof_sub. apply ApowerAx. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)