proposition: Lemma set_ext X Y : Subq X Y /\ Subq Y X <-> X = Y.
proof: Proof. split; intros H; try now rewrite H. destruct H as [H1 H2]. apply Aeq_p1_eq, Aeq_ext; now apply ASubq_Subq_p1. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms