Proofgold Proof

pf
Claim L0: ∀ x0 . Permutation x0 ⟶ struct_u x0 Let x0 of type ι be given. Assume H0: Permutation x0. Apply H0 with struct_u x0. Assume H1: struct_u x0. Assume H2: unpack_u_o x0 (λ x1 . bij x1 x1). The subproof is completed by applying H1. Apply unknownprop_137f848bdb78f472068da9f3e5698255d8403888e1b30f209fd7da0af03ad2f1 with Permutation. The subproof is completed by applying L0. ■