proposition: Lemma isaprop_isaroot {V : hSet} (E : hrel V) (r : V) : isaprop (isaroot E r).
proof: Proof. repeat (apply impred ; intros). apply propproperty. Qed.
imports: UniMath.Foundations.PartB UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.HLevels UniMath.Combinatorics.WellOrderedSets UniMath.Combinatorics.OrderedSets UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions