case succ i IH =>
  intro X Y
  simp
  intro X_sub_Y
  apply IH
  have := List.map_subset f X_sub_Y
  intro a a_in
  aesop
α : Type u_1
f : α → List α
i : ℕ
IH : ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i] X ⊆ (fun X => (List.map f X).join)^[i] Y
⊢ ∀ (X Y : List α), X ⊆ Y → (fun X => (List.map f X).join)^[i + 1] X ⊆ (fun X => (List.map f X).join)^[i + 1] Y
no goals