include "joint/linearise.ma".
include "LTL/LTL_paolo.ma".
include "LIN/LIN_paolo.ma".

definition ltl_to_lin : ltl_program → lin_program ≝
 λp. transform_program … p
  (λvarnames. transf_fundef … (linearise_int_fun ltl_lin_params varnames)).