include "ERTL/ERTL.ma".
include "LTL/LTL.ma". 
 
axiom translate_ertl_func:
  ∀globals: list ident.
    list (ident × ertl_function) → list (ident × (ltl_function_definition globals)).
  
definition translate: ∀e: ertl_program. ltl_program (ertl_pr_vars e) ≝
  λp.
    let globals ≝ map ? ? \fst (ertl_pr_vars p) in
    let ltl_pr_funcs ≝ map ? ? ? (ertl_pr_funcs p) in
      mk_ltl_program (ertl_pr_vars p) ltl_pr_funcs (ertl_pr_main p).
    # H1
    @ (translate_ertl_func globals) in ⊢ (? × %) (* dpm here *)