tweaks for type checking
added typed and untyped variables to exp
proving well typed exp theorem
trying to prove ST transitivity... going to barely tweak Proves
strengthened rem in Proves
formula written
formula through Proves
updating facts w/ formula
question/assume added
fact => datum for clarity (too many f's w/ fact & formula)
fixing weight lemmas
fixing proof_weights for Proves
Proves updated w/ formula