fact: Definition weakly_well_founded {X} (lt : X -> X -> Type) := ∏ P : X -> hProp, hereditary lt P -> ∏ x, P x.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Univalence