 			return a.typecheck(locals, globals)
 				.flatMap { t in
 					t.expression.analysis(
-						ifPi: { i, v, f in b.typecheck(locals, globals, against: v).map { f.substitute($0) } },
+						ifPi: { i, v, f in b.typecheck(locals, globals, against: v).map { f.substitute(i, $0) } },
 						otherwise: const(Either.left("illegal application of \(a) : \(t) to \(b)")))
 				}
 		case let .Pi(i, t, b):

			return a.typecheck(locals, globals)
				.flatMap { t in
					t.expression.analysis(
						ifSigma: { i, v, f in Either.right(b ? f.substitute(v) : v) },
						otherwise: const(Either.left("illegal projection of \(a) : \(t) field \(b ? 1 : 0)")))
				}
		case let .Sigma(i, a, b):



	// MARK: Substitution

	private func substitute(i: Int, _ term: Term) -> Term {
		return mapBoundVariables { depth, variable in
