{F : Type u_6} →
  {α : Type u_7} →
    {β : Type u_8} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : FunLike F α β] →
            {motive : ContinuousOpenMapClass F α β → Sort u} →
              (t : ContinuousOpenMapClass F α β) →
                ([toContinuousMapClass : ContinuousMapClass F α β] → (map_open : ∀ (f : F), IsOpenMap ⇑f) → motive ⋯) →
                  motive t