[Typer] [Git][monnier/typer][bosn] 3 commits: Clarified lem:S-equiv; boxed definition of translation in fig:[]