diff --git a/demonstration/ECopyValues.dfy b/demonstration/ECopyValues.dfy
index db27048513abe793b84ce5d9604d37894392a5f7..8f550bc8edeef999bc840d24bc32b44080bf94f5 100644
--- a/demonstration/ECopyValues.dfy
+++ b/demonstration/ECopyValues.dfy
@@ -5,7 +5,16 @@ method CopyValues<T, U>(mapping: map<T, U>, sources: map<T, T>) returns (updated
 {
   var result := map[];
   var remaining := set key | key in mapping :: key;
-  while |remaining| > 0 {
+  while |remaining| > 0
+    invariant
+      forall d | d in remaining ::
+      d in sources ==>
+      sources[d] in mapping
+    invariant
+      forall d | d in remaining ::
+      d !in sources ==>
+      d in mapping
+  {
     var destinationKey :| destinationKey in remaining;
     remaining := remaining - {destinationKey};
     var sourceKey := destinationKey;