private void constructorHelper(subExpression thm, subExpression tbe) throws IllegalInferenceException{
		if (tbe == null) {
			throw new IllegalInferenceException("Bad theorem application "+errorPrinting());
		} else if (thm.isVariable()) {
			try {
				if ((subValues.containsKey(thm.getName())) && 
						(!(subValues.get(thm.getName()).toString().equals(tbe.toString())))) {
					throw new IllegalInferenceException("Bad theorem application "+ errorPrinting());
				}
				subValues.put(thm.getName(),tbe);
			} catch (NullPointerException e) {
				throw new IllegalInferenceException("Bad theorem application "+errorPrinting());
			}
		} else if (thm.getName().equals("~")) {
			try {
				constructorHelper(thm.getLeft(),tbe.getLeft());
			} catch (NullPointerException e) {
				throw new IllegalInferenceException("Bad theorem application "+errorPrinting());
			}
		} else {
			try {
				constructorHelper(thm.getLeft(),tbe.getLeft());
				constructorHelper(thm.getRight(),tbe.getRight());
			} catch (NullPointerException e) {
				throw new IllegalInferenceException("Bad theorem application "+errorPrinting());
			}
		}
	}