fact: Definition wf (T : Type) : Type := ∑ lt : T -> T -> Type, (∏ x y z: T, lt x y -> lt y z -> lt x z) × (∏ h : (nat -> T), (∏ n : nat, lt (h (S n)) (h n)) -> Flse).
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs