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