Require Map.
Extraction Inline Map_rec.