proposition: Lemma repAx R X Y : functional R -> IN Y (Srep R X) <-> exists Z, IN Z X /\ R Z Y.
proof: Proof. intros H. unfold Srep. rewrite replAx. split; intros [Z[H1 H2]]; exists Z; split. - now apply sepAx in H1. - apply sepAx in H1 as [_ [Y' H']]. subst. eapply descAx; firstorder eauto. - apply sepAx; split; trivial. now exists Y. - eapply H; eauto. eapply descAx; firstorder eauto. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms