∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {J : Type u_4} [inst_3 : Fintype J] {X : J → C}
  {c : CategoryTheory.Limits.Bicone X} (hc : c.IsBilimit) (Y : C) (n : ℕ) (x : CategoryTheory.Abelian.Ext c.pt Y n),
  (fun e => ∑ i, (CategoryTheory.Abelian.Ext.mk₀ (c.π i)).comp (e i) ⋯)
      ((fun e i => (CategoryTheory.Abelian.Ext.mk₀ (c.ι i)).comp e ⋯) x) =
    x