∀ {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite))
  (X : Type u_1) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (h : ℕᵒᵖᵒᵖ) (j : ℕᵒᵖᵒᵖ)
  (xi : ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X)).obj h)
  (xj : ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X)).obj j),
  ((LightCondensed.locallyConstantPresheaf X).mapCocone c.op).ι.app h xi =
      ((LightCondensed.locallyConstantPresheaf X).mapCocone c.op).ι.app j xj →
    ∃ k f g,
      ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X)).map f xi =
        ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X)).map g xj