 			return ifPi(type.value, body)
 		case let .Sigma(type, body):
 			return ifSigma(type.value, body)
-		case let .Neutral(n):
-			return ifNeutral(n.value)
+		case let .Free(n):
+			return ifFree(n)
 		}
 	}
 

			ifSigma: { type, f in
				Term(Checkable.Sigma(Box(type.quote(n)), Box(f(.free(.Quote(n))).quote(n + 1))))
			},
			ifNeutral: {
				$0.quote(n)
			})
	}


			ifType: { ifType?($0) ?? otherwise() },
			ifPi: { ifPi?($0) ?? otherwise() },
			ifSigma: { ifSigma?($0) ?? otherwise() },
			ifFree: { ifFree?($0) ?? otherwise() })
	}


