more tweaks

jsiek · Jan 9, 2025 · b744421 · b744421
1 parent 947da7e
commit b744421
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/doc/ProofIntro.md b/doc/ProofIntro.md
@@ -902,10 +902,10 @@ switch on, as in `switch x` below.
 
     arbitrary x:Nat
     switch x {
-      case zero {
+      case 0 assume xz: x = 0 {
         ?
       }
-      case suc(x') {
+      case suc(x') assume xs: x = suc(x') {
         ?
       }
     }