{A} (R : Lt A) (a : A) := acc : (forall b, b < a -> R b) -> R a. Global Instance ishprop_Accessible `{Funext} {A} (R : Lt A) (a : A) : IsHProp ( R a). Proof. apply hprop_allpath. intros acc1. induction acc1 as [a acc1' IH]. intros [acc2']. apply ap. apply path_forall; intros b. apply path_forall; intros Hb. apply IH. Qed.
From HoTT Require Import TruncType ExcludedMiddle Modalities.ReflectiveSubuniverse abstract_algebra. From HoTT Require Import Universes.Smallness. From HoTT Require Import Colimits.Quotient. From HoTT Require Import HSet.