Partial commit bringing the agda development back in sync with the Twelf development in the paper. Nice simplificaiton to cut+ by changing the definition of suspnormalGamma, and brought subst+ and subst- into Foc.agda in order to phrase the eta+ case of cut admissibility as a use of focal substitution, not a use of contraction, like the paper does.