improved proofs, using equivalent formulation of round-trip laws for partial bijections