[Typer] [Git][monnier/typer][bosn] 3 commits: Prettified boxes; fixed PTS definition; added impredicative R; gave explanations on E- vs R- rules