change "context" so it keeps track of LF types and TS types in separate lists
add tactic tn1 (gets type of next argument and inserts it in the hole); use it in TS7.ts