Require Map.
Extraction Inline Map_rec Map_rect.