∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} [inst_2 : SizeOf X] [inst_3 : SizeOf Y] [inst_4 : (a : C(X, Y)) → SizeOf (P a)]
  (toHomotopy : f₀.Homotopy f₁)
  (prop' : ∀ (t : ↑unitInterval), P { toFun := fun x => toHomotopy.toFun (t, x), continuous_toFun := ⋯ }),
  sizeOf { toHomotopy := toHomotopy, prop' := prop' } = 1 + sizeOf toHomotopy