proposition: Lemma preZFS_Branch_issuperrigid (T : preZFS) (x : T) : issuperrigid (preZFS_Branch T x).
proof: Proof. split. - apply (pr1contr_to_contr _ (λ x, (isatree x ,, isaprop_isatree x)) (preZFS_Branch T x)). apply (iscontrauto_Tree_TRRGraph (Up x) ((pr222 T) x)). - intros y. apply (pr1contr_to_contr _ (λ x, (isatree x ,, isaprop_isatree x)) (Up y)). simpl. unfold preZFS_Branch. unfold preZFS_Branch in y. rewrite <- UpUpid. apply (iscontrauto_Tree_TRRGraph (Up (pr1 y)) ((pr222 T) (pr1 y))). 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