rewrote all rewrites :P  using cong+sym+trans and coerce. Correctness last hole should be easier