English
For every nested list l in Lists' α true, embedding the flat list back yields the original: ofList(toList(l)) = l.
Русский
Для каждого вложенного списка l типа Lists' α true внедрение плоского списка обратно даёт исходный вложенный список: ofList(toList(l)) = l.
LaTeX
$$$\\operatorname{ofList}(\\operatorname{toList}(l)) = l$$$
Lean4
@[simp]
theorem of_toList : ∀ l : Lists' α true, ofList (toList l) = l :=
suffices
∀ (b) (h : true = b) (l : Lists' α b),
let l' : Lists' α true := by rw [h]; exact l
ofList (toList l') = l'
from this _ rfl
fun b h l => by
induction l with
| atom => cases h
| nil => simp
| cons' b a _ IH => simpa [cons] using IH rfl
