Define translation operator; stage the proof to be bidirectional; replace correspondance between PTS's with lemmas of injective maps between sorts and axioms of CCw and Typer