case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ unzip l = unzipTR l
⊢ @unzip = @unzipTR
funext α β l
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ unzip l = foldr (fun x x_1 => (x.fst :: x_1.fst, x.snd :: x_1.snd)) ([], []) l
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ unzip l = unzipTR l
simp [unzipTR]
no goals
case h.h.h
α : Type u_2
β : Type u_1
l : List (α × β)
⊢ unzip l = foldr (fun x x_1 => (x.fst :: x_1.fst, x.snd :: x_1.snd)) ([], []) l
induction l <;> simp [*]