∀{l}{A B C : Set l} -> (f : B -> C) -> (g : A -> B) -> (ls : List A) -> map (f g) ls ≡ map f (map g ls)
が型で、この型にあった関数を見つけることが証明になることがカリーハワード対応なんだよ