∀ {α : Type u_1} {ι : Sort u_2} {β : Sort u_3} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {T : Set α}
  (hT' : T = Set.iUnion S),
  Directed (fun x1 x2 => x1 ≤ x2) S →
    ∀ (op : ↑T → ↑T → ↑T) (opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)),
      (∀ (i : ι) (x y : ↑(S i)), Set.inclusion ⋯ (opi i x y) = op (Set.inclusion ⋯ x) (Set.inclusion ⋯ y)) →
        ∀ (opβ : β → β → β),
          (∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)) →
            ∀ (x y : ↑T),
              Set.iUnionLift S f hf T ⋯ (op x y) = opβ (Set.iUnionLift S f hf T ⋯ x) (Set.iUnionLift S f hf T ⋯ y)