∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)],
  (Pretrivialization.codExtend' hs e).baseSet = Subtype.val '' e.baseSet