Definition isweq_Branch_of_Branch_to_Branch {T : preZFS} (x : T) (y : Branch T x) : isweq (Branch_of_Branch_to_Branch x y). Proof. set (f := Branch_of_Branch_to_Branch x y). set (g := Branch_of_Branch_to_Branch_inv x y). assert (L : ∏ x, f (g x) = x). { intros z. unfold f ; unfold Branch_of_Branch_to_Branch. unfold g ; unfold Branch_of_Branch_to_Branch_inv. induction z as [z π]. simpl. apply idpath. } assert (LL : ∏ x, g (f x) = x). { intros z. unfold f ; unfold Branch_of_Branch_to_Branch. unfold g ; unfold Branch_of_Branch_to_Branch_inv. simpl. induction z as [z π]. apply total2_paths_equiv. assert (H : (pr1 z,, pr122 (pr221 (pr1 T)) x (pr1 y) (pr1 z) (pr2 y) π) = z). { apply total2_paths_equiv. exists (idpath (pr1 z)). apply propproperty. } exists H. apply propproperty. } apply (@weq_iso _ _ _ _ LL L). Defined.