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