proposition: Lemma ASubq_Subq_p1 X Y : ASubq (proj1_sig Y) (proj1_sig X) <-> Subq Y X.
proof: Proof. split; intros H Z H1. - apply Ain_IN_p1, H. auto. - apply IN_Ain_NS_p1, H. auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms