proposition: Lemma maxidom (w : wfs) : ∏ (x : uset w), wfs_wf_uord (maxi_fun w x) w.
proof: Proof. intro x. exists (fun (z : uset (maxi_fun w x)) => pr1 z). split. - intros x0 y p. exact p. - exists x. intro x0. exact (pr2 x0). Defined.
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs