obligation 2

  Next Obligation.
    unfold mmap_to_equation in Heq_anonymous.
    destruct (
        mmap
          (to_equation
             (Env.adds' (L.n_vars n)
                        (Env.adds' (L.n_in n)
                                   (Env.from_list (L.n_out n))))
             (fun x : Env.key =>
                if
                  Env.mem x (Env.from_list (L.n_out n))
                then
                  Error
                    (msg
                       "output variable defined as a fby")
                else OK tt)) (L.n_eqs n)
      ) eqn:?; try discriminate.
    monadInv Heq_anonymous. revert out0 H.
    intros xo Hin.
    monadInv Heqr. induction H as [| eq leq eq' leq' Htoeq ].
    intro Hbad. inv Hbad.
    assert (Hmmap := Heqr).
    apply mmap_cons2 in Heqr.
    destruct Heqr as (eq'' & leq'' & Heqs' & Htoeq' & Hmmap').
    inv Heqs'.
    simpl. destruct (NL.is_fby eq') eqn:?.
    - unfold NL.vars_defined, flat_map. simpl. rewrite in_app.
      intro Hi. destruct Hi.
      + unfold to_equation in Htoeq. destruct eq''.
        cases_eqn E; monadInv1 Htoeq; inv Heqb.
        simpl in H0. destruct H0; auto. subst. inv EQ.
        apply Env.Props.P.F.not_mem_in_iff in E8. apply E8.
        rewrite in_map_iff in Hin.
        destruct Hin as ((x & ?) & Hfst & Hin). inv Hfst.
        eapply Env.find_In. eapply Env.In_find_adds'; simpl; eauto.
        destruct n. simpl. assert (Hnodup := n_nodup).
        now repeat apply NoDupMembers_app_r in Hnodup.
      + apply IHlist_forall2; auto.
    - apply IHlist_forall2; eauto.