proposition: Lemma replAx F X Y : IN Y (Srepl F X) <-> exists Z, IN Z X /\ Y = F Z.
proof: Proof. Proof with try apply emfun_Aeq. split; intros H. - apply IN_Ain_p1_NS, AreplAx in H as [z[Z1 Z2]]... exists (NS z). split; auto. now apply Aeq_p1_eq. - destruct H as [Z[Z1 Z2]]. apply Ain_IN_p1_NS, AreplAx... exists (proj1_sig Z). split; auto. rewrite Z2. unfold emfun. now rewrite NS_p1_eq. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms