 		return analysis(
 			ifType: const(.type),
 			ifBound: { Term(.Variable(n - $0 - 1)) },
-			ifPi: { type, f in Term(.Pi(n, Box(type.quote(n)), Box(f(.Bound(n))!.quote(n + 1)))) },
-			ifSigma: { type, f in Term(.Sigma(n, Box(type.quote(n)), Box(f(.Bound(n))!.quote(n + 1)))) })
+			ifFree: { Term(.Variable($0)) },
+			ifPi: { type, f in Term(.Pi(n, Box(type.quote(n)), Box(f(.Free(n))!.quote(n + 1)))) },
+			ifSigma: { type, f in Term(.Sigma(n, Box(type.quote(n)), Box(f(.Free(n))!.quote(n + 1)))) })
 	}
 
 

			return ifType()
		case let .Bound(n):
			return ifBound(n)
		case let .Pi(type, body):
			return ifPi(type.value, body)
		case let .Sigma(type, body):


	case Type
	case Bound(Int)
	case Free(Int)
	case Pi(Box<Value>, Value -> Value?)
	case Sigma(Box<Value>, Value -> Value?)
}
