made some proofs transparent, simplifying some subsequent proofs for inverses of morphisms