α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ nil → ofList (toList l) = nil
α : Type u_1
l : Lists' α true
⊢ l ⊆ nil → l = nil
rw [← of_toList l]
case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil

case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil
α : Type u_1
l : Lists' α true
⊢ ofList (toList l) ⊆ nil → ofList (toList l) = nil
induction toList l <;> intro h
no goals
case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil
rfl
no goals
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil
rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩