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