proposition: Lemma descAx2 (P P' : SET -> Prop) : (forall x, P x <-> P' x) -> desc P = desc P'.
proof: Proof. intros H. apply Aeq_NS_eq, Aeq_ref', TDesc2. intros s. apply H. Qed.
imports: Undecidability.FOL.Sets.Models(Aczel) Setoid Morphisms