∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) (A : C) (a : (F.obj A).carrier)
  (isGalois : CategoryTheory.PreGaloisCategory.IsGalois A) (B : C) (b : (F.obj B).carrier)
  (isGalois_1 : CategoryTheory.PreGaloisCategory.IsGalois B)
  (motive :
    (Opposite.op { obj := A, pt := a, isGalois := isGalois } ⟶
        Opposite.op { obj := B, pt := b, isGalois := isGalois_1 }) →
      Prop)
  (x :
    Opposite.op { obj := A, pt := a, isGalois := isGalois } ⟶
      Opposite.op { obj := B, pt := b, isGalois := isGalois_1 }),
  (∀
      (f :
        (Opposite.unop (Opposite.op { obj := B, pt := b, isGalois := isGalois_1 })).obj ⟶
          (Opposite.unop (Opposite.op { obj := A, pt := a, isGalois := isGalois })).obj)
      (hf : (CategoryTheory.ConcreteCategory.hom (F.map f)) b = a), motive (Opposite.op { val := f, comp := hf })) →
    motive x