Index: src/SynTree/TypeSubstitution.cc
===================================================================
--- src/SynTree/TypeSubstitution.cc	(revision 77bfc801f3cb89b3b5dcb4ce8808bf2332aeef24)
+++ src/SynTree/TypeSubstitution.cc	(revision b869ec5003199dfa8bcbc3e90cae94d2d8ad1127)
@@ -62,4 +62,8 @@
 	} // if
 	typeEnv[ formalType ] = actualType->clone();
+}
+
+void TypeSubstitution::addVar( std::string formalExpr, Expression *actualExpr ) {
+	varEnv[ formalExpr ] = actualExpr;
 }
 
Index: src/SynTree/TypeSubstitution.h
===================================================================
--- src/SynTree/TypeSubstitution.h	(revision 77bfc801f3cb89b3b5dcb4ce8808bf2332aeef24)
+++ src/SynTree/TypeSubstitution.h	(revision b869ec5003199dfa8bcbc3e90cae94d2d8ad1127)
@@ -48,4 +48,6 @@
 	bool empty() const;
 
+	void addVar( std::string formalExpr, Expression *actualExpr );
+
 	template< typename FormalIterator, typename ActualIterator >
 	void add( FormalIterator formalBegin, FormalIterator formalEnd, ActualIterator actualBegin );
@@ -89,4 +91,9 @@
 	auto begin() const -> decltype( typeEnv.begin() ) { return typeEnv.begin(); }
 	auto   end() const -> decltype( typeEnv.  end() ) { return typeEnv.  end(); }
+
+	auto beginVar()       -> decltype( varEnv.begin() ) { return varEnv.begin(); }
+	auto   endVar()       -> decltype( varEnv.  end() ) { return varEnv.  end(); }
+	auto beginVar() const -> decltype( varEnv.begin() ) { return varEnv.begin(); }
+	auto   endVar() const -> decltype( varEnv.  end() ) { return varEnv.  end(); }
 };