Update error message text

Author: tchajed

src/lec1_logic.dfy

@@ -102,7 +102,7 @@ lemma AbsStrictlyLarger_attempt(x: int)
   // other languages.
   if x < 0 {
     // there's no error here! the postcondition actually does hold on this path
-  } else { // error: a postcondition might not hold on this return path
+  } else { // error: a postcondition could not be proved on this return path
     // But here, if we think about it, we realize abs(x) == x.
     assert abs(x) == x;
   }

src/lec2_sequences.dfy

@@ -76,7 +76,7 @@ lemma CheckedPreconditions(s: seq<int>, i: nat)
 lemma CheckedFunctionPreconditions(s: seq<int>, i: nat)
   // almost same as above, but notice that the error specifically points to the
   // `SeqGet` precondition
-  requires SeqGet(s, i) > 0 // error: function precondition might not hold
+  requires SeqGet(s, i) > 0 // error: function precondition could not be proved
 {}
 
 lemma SequenceAppendFact(s1: seq<int>, s2: seq<int>)

src/lec3_algebraic_datatypes.dfy

@@ -160,7 +160,7 @@ lemma MilkDrink_spec_v1(coffee: CoffeeRecipe)
   match coffee {
     case Latte(milk) => {}
     case Espresso(drip) => {}
-    case Drip(oz, milk) => { // error: A postcondition might not hold on this return path
+    case Drip(oz, milk) => { // error: A postcondition could not be proved on this return path
       // the error message pinpoints this case
     }
   }