understand inversion! gives you hypotheses about the way things must have een constructed. nice proof: ev_ev__ev. rewrite it