[Typer] [Git][monnier/typer][bosn] 3 commits: Define translation operator; stage the proof to be bidirectional; replace…