Goal:
    f : Edge.t -> Edge.t  es : EdgeSet.t  e : EdgeSet.elt
  ============================
   ((exists x : Edge.t, f x = e /\ In x (EdgeSetProp.to_list es)) ->
    exists e0 : Edge.t, e = f e0 /\ EdgeSet.In e0 es)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrmove@1> $1 $2
DEBUG LTAC Evaluated term: EdgeSetProp.of_list_1
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=InA eq e (map f (EdgeSetProp.to_list es)))
                              (EdgeSetProp.of_list_1
                                 (map f (EdgeSetProp.to_list es)) e)
                              _view_subject_)
DEBUG LTAC Evaluated term: InA_In_eq
DEBUG LTAC Evaluated term: (iffLR (Q:=In e (map f (EdgeSetProp.to_list es)))
                              (InA_In_eq e (map f (EdgeSetProp.to_list es)))
                              (iffLR
                                 (Q:=InA eq e
                                       (map f (EdgeSetProp.to_list es)))
                                 (EdgeSetProp.of_list_1
                                    (map f (EdgeSetProp.to_list es)) e)
                                 _view_subject_))
DEBUG LTAC Evaluated term: in_map_iff
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=exists x : Edge.t,
                                    f x = e /\ In x (EdgeSetProp.to_list es))
                              (in_map_iff f (EdgeSetProp.to_list es) e)
                              (iffLR
                                 (Q:=In e (map f (EdgeSetProp.to_list es)))
                                 (InA_In_eq e
                                    (map f (EdgeSetProp.to_list es)))
                                 (iffLR
                                    (Q:=InA eq e
                                          (map f (EdgeSetProp.to_list es)))
                                    (EdgeSetProp.of_list_1
                                       (map f (EdgeSetProp.to_list es)) e)
                                    _view_subject_)))