Types initial commit
Typed arith. expressions, value is NF, step deterministic
Typing
Progress
Preservation
Soundness
Normalize tactic