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

definition ltl_to_lin : ltl_program → lin_program ≝
  linearise ….