fact: Definition wfs_wf_uord (v : wfs) (w : wfs) : Type := ∑ f : uset v -> uset w, (∏ x y : uset v, (uord v) x y -> (uord w) (f x) (f y)) × (∑ y : uset w, ∏ (x: uset v), (uord w) (f x) y).
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs