case H0
α : Type u
β : Type v
γ : Type w
⊢ [] <+ sublists []

case H1
α : Type u
β : Type v
γ : Type w
l : List α
a : α
ih : map List.ret l <+ sublists l
⊢ map List.ret l ++ [List.ret a] <+ sublists l ++ map (fun x => x ++ [a]) (sublists l)
α : Type u
β : Type v
γ : Type w
l : List α
⊢ map List.ret l <+ sublists l
induction' l using reverseRecOn with l a ih <;>
simp only [map, map_append, sublists_concat]
no goals
case H1
α : Type u
β : Type v
γ : Type w
l : List α
a : α
ih : map List.ret l <+ sublists l
⊢ map List.ret l ++ [List.ret a] <+ sublists l ++ map (fun x => x ++ [a]) (sublists l)
exact ((append_sublist_append_left _).2 <|
            singleton_sublist.2 <| mem_map.2 ⟨[], mem_sublists.2 (nil_sublist _), by rfl⟩).trans
        ((append_sublist_append_right _).2 ih)
no goals
case H0
α : Type u
β : Type v
γ : Type w
⊢ [] <+ sublists []
simp only [sublists_nil, sublist_cons]
no goals
α : Type u
β : Type v
γ : Type w
l : List α
a : α
ih : map List.ret l <+ sublists l
⊢ [] ++ [a] = List.ret a
rfl