--- a/src/DataStruct.v	Sun Apr 21 16:09:55 2019 -0400
+++ b/src/DataStruct.v	Sun Feb 02 10:46:14 2020 -0500
@@ -294,7 +294,7 @@
 
 (** Now we can define a type family for expressions.  An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts].  We effectively use the de Bruijn index variable representation%~\cite{DeBruijn}%.  Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *)
 
-Inductive exp : list type -> type -> Set :=
+Inductive exp : list type -> type -> Type :=
 | Const : forall ts, exp ts Unit
 (* begin thide *)
 | Var : forall ts t, member t ts -> exp ts t