Definition downward_closure : downward_closed_subtype P := make_downward_closed_subtype P _ downward_closure_is_downward_closed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All.