P
Initializing...
Algorithmic typing lacks subject reduction · Prove2Me