private void assignHypotheses(final List<Expression> hypotheses, final Substituter substituter)
	throws VerifyException {
		final int size = hypotheses.size();
		final int start = proofStack.size() - size;
		if (start < 0) {
			try {
				feed.reject("Too few hypotheses on stack");
			} catch (ScannerException ignored) {
				logger.error("Too few hypotheses on stack");
			}
			logger.debug("Hypotheses missing: " + -start);
			throw new VerifyException("Too few hypotheses on stack");
		}
		try {
			for (int i = 0; i != size; ++i)
				substituter.unify(hypotheses.get(i).totalUnfold(), proofStack.get(start + i));
			proofStack.setSize(start);
		} catch (UnifyException e) {
			try {
				feed.reject("Unification error while popping hypotheses from proof stack: " + e.getMessage());
			} catch (ScannerException ignored) {
				logger.error("Unification error while popping hypotheses from proof stack: " + e.getMessage());
			}
			logger.debug("Source expression: " + e.getSource());
			logger.debug("Target expression: " + e.getSource());
			throw new VerifyException("Unification error while popping hypotheses from proof stack", e);
		}
	}