Proposition all_inr_directed_set_map_eq_help (i : D) (y : Y) (r : inr y = D i) : all_inr_directed_set_map_help i (inr y) r = y. Proof. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.