proposition: Lemma succ_eq s : succ (classof s) = classof (Asucc s).
proof: Proof. apply set_ext. split; intros X H. - apply unionAx in H as [Y[H1 H2]]. destruct (classof_ex X) as [t ->]. apply classof_ele. apply AunionAx. apply upairAx in H1 as [->| ->]. + exists s. split; try now apply classof_ele. apply AupairAx. now left. + exists (Aupair s s). rewrite AupairAx. split; auto. apply upairAx in H2. rewrite !classof_eq in H2. now apply AupairAx. - destruct (classof_ex X) as [t ->]. apply classof_ele in H. apply AunionAx in H as [u[H1 H2]]. apply unionAx. apply AupairAx in H1 as [H1| H1]; subst. + exists (classof u). split; try now apply classof_ele. apply upairAx. left. now apply classof_eq. + exists (upair (classof s) (classof s)). rewrite upairAx. split; auto. rewrite H1 in H2. apply AupairAx in H2. rewrite <- !classof_eq in H2. now apply upairAx. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel)