proposition: Lemma upairAx X Y Z : IN Z (Supair X Y) <-> Z = X \/ Z = Y.
proof: Proof. split; intros H. - apply IN_Ain_p1_NS, AupairAx in H as [H|H]. + left. now apply Aeq_p1_eq. + right. now apply Aeq_p1_eq. - apply Ain_IN_p1_NS, AupairAx. destruct H as [-> | ->]; auto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms