Lemma downward_closure_is_downward_closed : is_downward_closed P downward_closure_hsubtype. Proof. intros y z. use (hinhfun _ (pr2 y)). intro Hy. exists (pr1 Hy). refine (istrans_po P _ _ _ (pr2 z) (pr2 Hy)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All.