Lemma preZFS_Branch_issuperrigid (T : preZFS) (x : T) : issuperrigid (preZFS_Branch T x). 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.