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