Theorem: Cpdt.Chapter8.IList.inject_unject_inv (Cpdt/Chapter8/LengthIndexed.lean)

State before:
α✝ : Type
xs : List α✝
⊢ (unject (inject xs)).val = xs
Tactic:
induction xs <;> simp_all[unject, inject]
State after:
no goals