proposition: Lemma isaprop_isatree (G : TRRGraph) : isaprop (isatree G).
proof: Proof. apply impred. intros t ; apply impred. intros x ; apply impred. intros y ; apply isapropdirprod. - apply impred. intros P. apply setproperty. - 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