diff --git a/acl.cool/site/css-sample.dj b/acl.cool/site/css-sample.dj index c5f00a1..b1b42b5 100644 --- a/acl.cool/site/css-sample.dj +++ b/acl.cool/site/css-sample.dj @@ -21,7 +21,7 @@ def map' {α β : Type} (f : α → β) : List α → List β | [] => [] | 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 intro xs f g induction xs