Proposition intrinsic_apartness_not_eq {x y : X} (p : x # y) : ¬(x = y). Proof. intro q. induction q. exact (irrefl_intrinsic_apartness x p). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.