fix proofs of side conditions of REPL translation

needed to eta a higher-order call to MAP in build_ctor_tenv_def, and
prove some extra conditions in the type inferencer. apart from that,
some things just got more arguments.