no goals
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ length (sublists' (a :: l)) = 2 ^ length (a :: l)
simp_arith only [sublists'_cons, length_append, length_sublists' l,
  length_map, length, Nat.pow_succ', mul_succ, mul_zero, zero_add]