Require  Import exo_inter.
Require  Import exo_induc_fct.

Recursive Extraction Library exo_inter.
Recursive Extraction Library exo_induc_fct.