∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)),
  (CategoryTheory.PreOneHypercover.cylinder f g).X p = CategoryTheory.PreOneHypercover.cylinderX f g p.snd