Goal:
  
  f : EdgeSet.elt -> EdgeSet.elt
  es : EdgeSet.t
  e : EdgeSet.elt
  __view_subject_1_ : In e (EdgeSet.elements es)
  ============================
   (EdgeSet.In (f e) (edge_map f es))


DEBUG:Going to execute:
apply /EdgeSetProp.of_list_1 
DEBUG LTAC Evaluated term: EdgeSet.elements_spec1
DEBUG LTAC Evaluated term: (iffRL (P:=InA eq e (EdgeSet.elements es))
                              (EdgeSet.elements_spec1 es e) _view_subject_)
DEBUG LTAC Evaluated term: InA_In_eq
DEBUG LTAC Evaluated term: (iffLR (Q:=In e (EdgeSet.elements es))
                              (InA_In_eq e (EdgeSet.elements es))
                              (iffRL (P:=InA eq e (EdgeSet.elements es))
                                 (EdgeSet.elements_spec1 es e) _view_subject_))