proposition: Lemma isaprop_issuperrigid (T : Tree) : isaprop (issuperrigid T).
proof: Proof. unfold issuperrigid. apply isapropdirprod. apply isaprop_isrigid. apply impred. intros t. apply isaprop_isrigid. 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