∀ {I : Type u_1} [inst : CategoryTheory.SmallCategory I] {F : CategoryTheory.Functor I FintypeCat}
  (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite))
  (motive : CategoryTheory.StructuredArrow c.pt FintypeCat.toProfinite → Prop)
  (h : CategoryTheory.StructuredArrow c.pt FintypeCat.toProfinite),
  (∀ (left : CategoryTheory.Discrete PUnit.{1}) (X : FintypeCat) (f : c.pt ⟶ FintypeCat.toProfinite.obj X),
      motive { left := left, right := X, hom := f }) →
    motive h