Fill in some proofs in TS7-relative.ts, based on the proofs of TS7.ts
The translation of proofs is mechanical, so the simplicity of the type
in relative mode might mean it's the encoding to choose now.
return to treating "_" as just another variable name, in the type checker, because
tactics were incorporating such variables into the terms they return.
Thinking that Mode Relative is the choice, have decided to implement a tactic $shuffle
which will transform something like ($shuffle f x y) into (f x_1 y_1 CDR x_2 y_2),
and be developed further.