--- a/src/coq/Semantics.v	Sat Feb 21 13:17:06 2009 -0500
+++ b/src/coq/Semantics.v	Sat Feb 21 13:22:30 2009 -0500
@@ -209,5 +209,21 @@
         | right _ => fun x => x
       end ((eDen e1) n)
 
+    | Concat c1 c2 e1 e2 => fun n =>
+      match (cDen c1) n as D return match D with
+                                      | None => unit
+                                      | Some T => T
+                                    end
+      -> match (match D with
+                  | None => (cDen c2) n
+                  | v => v
+                end) with
+           | None => unit
+           | Some T => T
+         end with
+        | None => fun _ => (eDen e2) n
+        | _ => fun x => x
+      end ((eDen e1) n)
+
     | _ => cheat _
   end.

--- a/src/coq/Syntax.v	Sat Feb 21 13:17:06 2009 -0500
+++ b/src/coq/Syntax.v	Sat Feb 21 13:22:30 2009 -0500
@@ -187,6 +187,6 @@
   | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _)))
   | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t
   | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c')
-  | Concat : forall c1 c2, disj c1 c2 -> exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
+  | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
   | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c).
 End vars.