proposition: Lemma pasting_lemma_fn_right (x : X) (Hx0 : ~ In A x) (Hx1 : In B x) : pasting_lemma_fn x = g (exist B x Hx1).
proof: Proof. Proof using Type. unfold pasting_lemma_fn. destruct (classic_dec _); try contradiction. destruct (proof_irrelevance _ (Union_Full_set _ n) Hx1); reflexivity. Qed.
imports: ZornsLemma(CardinalsEns DecidableDec FiniteIntersections Proj1SigInjective) Topology(WeakTopology)