Goal:
  
  f : EdgeSet.elt -> EdgeSet.elt
  es : EdgeSet.t
  e : EdgeSet.elt
  __view_subject_1_ : In e (EdgeSet.elements es)
  ============================
   (InA eq (f e) (map f (EdgeSetProp.to_list es)))


DEBUG:Going to execute:
apply /InA_In_eq 
DEBUG LTAC Evaluated term: EdgeSetProp.of_list_1