∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e e' : Bundle.Pretrivialization F proj), e.toPartialEquiv = e'.toPartialEquiv → e.baseSet = e'.baseSet → e = e'