∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → SemilatticeSup (f i)]
  [inst_2 : (i : I) → Zero (f i)] (i : I) (x y : f i), Pi.single i (x ⊔ y) = Pi.single i x ⊔ Pi.single i y