Module MMproof

  eapply (
    MMtsosimproof.full_sim ma_sem mc_sem
      (fun sge tge => sge = tge /\ wt_genv sge)
      (fun sge tge => match_state tge)
      (fun sge tge => (ltof _ measure))
      mm_match_prg); intros.
  - intros. destruct GENVR as [-> _]. destruct MP as [-> _]. done.
  - intros. destruct MP as [-> WTP].
    exists tge. split. done. split. done.
    intros v f FF. simpl in INIT.
    eby exploit @Genv.find_funct_prop.
  - eapply Genv.initmem_allocated_global. apply INIT. edone.
  - destruct GENVR as [-> WT].
    destruct (thread_init_related WT INIT LD) as [si (SI & MS)].
    exists si. vauto.
  - destruct GENVR as [-> WT].
    apply (thread_init_related_none INITF LD).
  - destruct GR as [-> WT].
    by apply mc_ma_perthread_sim.
  - destruct GR as [-> _]. apply mc_ma_perthread_stuck_sim.
  - destruct GR as [-> _]. apply mem_eq_preserves_simrel.
  - apply well_founded_ltof.
Qed.