Comment by DamonHD

If your type checking was in the Martin-Löf school, and you started with a putative proof that what you wanted to execute was possible, then maybe! B^>