proposition: Lemma power_eqclass X : eqclass (power' X).
proof: Proof. Proof using ce. destruct (classof_ex X) as [s ->]. exists (Apower s). apply ce. intros t. split; intros H. - destruct H as [s'[H1 H2]]; simpl in H1. now rewrite H1, H2. - exists s. auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)