[Typer] [Git][monnier/typer][bosn] Separated Case 1 of proof into two; introducing Erasable constructor