proposition: Proposition irref (w : wfs) : ∏ (x : uset w), (uord w) x x -> Flse.
proof: Proof. intro x. intro p. exact (wfp w (fun n => x) (fun n => p)). Defined.
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs