proposition: Lemma descAx (P : SET -> Prop) X : P X -> unique P X -> P (desc P).
proof: Proof. intros H1 H2. enough (empred P (tdelta (empred P))) by assumption. apply TDesc1. exists (proj1_sig X). intros t. split; intros H. - apply NS_eq_Aeq_p1. symmetry. now apply H2. - symmetry in H. apply (empred_Aeq H). hnf. now rewrite NS_p1_eq. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms