intro X Y
α : Type u_1
f : α → List α
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y
α : Type u_1
f : α → List α
X Y : List α
⊢ X ⊆ Y → (fun X => (List.map f X).join)^[0] X ⊆ (fun X => (List.map f X).join)^[0] Y