α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ (do
      let x ← sublists l
      map (fun x_1 => x_1 ++ x) (sublists [a])) =
    do
    let x ← sublists l
    [x, a :: x]
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists ([a] ++ l) = do
    let x ← sublists l
    [x, a :: x]
rw [sublists_append]
no goals
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ (do
      let x ← sublists l
      map (fun x_1 => x_1 ++ x) (sublists [a])) =
    do
    let x ← sublists l
    [x, a :: x]
simp only [sublists_singleton, map_cons, bind_eq_bind, nil_append, cons_append, map_nil]