This commit is contained in:
Alexander 2025-06-14 11:44:15 -04:00
parent 93a32bd9bc
commit 177c2732b6

View file

@ -21,7 +21,7 @@ def map' {α β : Type} (f : α → β) : List α → List β
| [] => [] | [] => []
| x :: xs => f x :: map' f xs | x :: xs => f x :: map' f xs
theorem fuse {α β γ} : ∀ (xs : List α) (f : α → β) (g :β → γ), theorem fuse {α β γ} : ∀ (xs : List α) (f : α → β) (g : β → γ),
(map' g ∘ map' f) xs = map' (g ∘ f) xs := by (map' g ∘ map' f) xs = map' (g ∘ f) xs := by
intro xs f g intro xs f g
induction xs induction xs