proposition: Lemma powerAx X Y : IN Y (Spower X) <-> Subq Y X.
proof: Proof. split; intros H. - apply IN_Ain_p1_NS, ApowerAx in H. now apply ASubq_Subq_p1. - apply Ain_IN_p1_NS, ApowerAx. now apply ASubq_Subq_p1. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms