∀ (Map : (α : Type) → Type → [BEq α] → [Hashable α] → Type)
  (mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map α β)
  (mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → Option β)
  (mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → β → Map α β)
  (Set : (α : Type) → [BEq α] → [Hashable α] → Type)
  (mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set α)
  (setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Option α)
  (setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Set α)
  (Map_1 : (α : Type) → Type → [BEq α] → [Hashable α] → Type)
  (mkMap_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map_1 α β)
  (mapFind?_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map_1 α β → α → Option β)
  (mapInsert_1 : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map_1 α β → α → β → Map_1 α β)
  (Set_1 : (α : Type) → [BEq α] → [Hashable α] → Type)
  (mkSet_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set_1 α)
  (setFind?_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set_1 α → α → Option α)
  (setInsert_1 : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set_1 α → α → Set_1 α),
  ({ Map := Map, mkMap := mkMap, mapFind? := mapFind?, mapInsert := mapInsert, Set := Set, mkSet := mkSet,
        setFind? := setFind?, setInsert := setInsert } =
      { Map := Map_1, mkMap := mkMap_1, mapFind? := mapFind?_1, mapInsert := mapInsert_1, Set := Set_1,
        mkSet := mkSet_1, setFind? := setFind?_1, setInsert := setInsert_1 }) =
    (Map = Map_1 ∧
      mkMap ≍ mkMap_1 ∧
        mapFind? ≍ mapFind?_1 ∧
          mapInsert ≍ mapInsert_1 ∧ Set = Set_1 ∧ mkSet ≍ mkSet_1 ∧ setFind? ≍ setFind?_1 ∧ setInsert ≍ setInsert_1)