∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} [inst_1 : SizeOf C] {fst snd : S.Arrow} (r : fst.Relation snd),
  sizeOf { fst := fst, snd := snd, r := r } = 1 + sizeOf fst + sizeOf snd + sizeOf r