Add example showing that a function graph is equivalent to its fiber
Add example showing that a function graph is equivalent to its fiber

In general this requires a transparent proof of completeness of the
graph (not derived automatically yet).

mattam82/Coq-Equations,mattam82/Coq-Equations