proposition: Lemma maxi (w : wfs) : wfs_wf_uord w wfs_wf_t.
proof: Proof. exists (maxi_fun w). split. - exact (maxi_homo w). - exact (tpair _ _ (maxidom w)). Defined.
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs