Definition strongly_well_founded {X} (lt : X -> X -> Type) := ∏ (P : X -> Type) (H : hereditary lt P), ∑ (f : ∏ x, P x), ∏ x, f x = H x (λ y _, f y).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.