fact: Definition wfp (w : wfs) : (λ _ : ∏ x y z : pr1 w, pr1 (pr2 w) x y → pr1 (pr2 w) y z → pr1 (pr2 w) x z, ∏ h : nat → pr1 w, (∏ n : nat, pr1 (pr2 w) (h (S n)) (h n)) → Flse) (pr1 (pr2 (pr2 w))) := pr2 (pr2 (pr2 w)).
imports: UniMath.Foundations.All UniMath.Tactics.EnsureStructuredProofs