discharged an axiom about integers
change "Parameter" -> "Axiom" for logical assumptions
refactoring and documentation
completed the decomposition proof of timed typing