 		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)))) })
 	}
 
 

	public func analysis<T>(
		ifType: (() -> T)? = nil,
		ifBound: (Int -> T)? = nil,
		ifPi: ((Value, Value -> Value?) -> T)? = nil,
		ifSigma: ((Value, Value -> Value?) -> T)? = nil,
		@noescape otherwise: () -> T) -> T {
		return analysis(
			ifType: { ifType?() ?? otherwise() },
			ifBound: { ifBound?($0) ?? otherwise() },
			ifPi: { ifPi?($0) ?? otherwise() },
			ifSigma: { ifSigma?($0) ?? otherwise() })
	}


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