diff --git a/hermes/examples/abs.rs b/hermes/examples/abs.rs
index b015a95b65..91096340f1 100644
--- a/hermes/examples/abs.rs
+++ b/hermes/examples/abs.rs
@@ -7,16 +7,36 @@
 /// ensures (h2): (x : Int) < 0 -> (ret : Int) = -x
 /// proof (h_progress):
 ///   unfold abs
-///   split <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
+///   cases h_req
+///   have : (↑(0 : I32) : Int) = 0 := by rfl
+///   have := Aeneas.Std.IScalar.hmin x
+///   have := Aeneas.Std.IScalar.hmax x
+///   split
+///   · have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)
+///     split at h_bound <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg]); (try scalar_tac)
+///   · simp_all
 /// proof (h0):
 ///   unfold abs at h_returns
-///   split at h_returns <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
+///   have : (↑(0 : I32) : Int) = 0 := by rfl
+///   have := Aeneas.Std.IScalar.hmin x
+///   have := Aeneas.Std.IScalar.hmax x
+///   split at h_returns
+///   · have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)
+///     split at h_bound <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg]); (try scalar_tac)
+///   · simp_all
 /// proof (h1):
 ///   unfold abs at h_returns
-///   split at h_returns <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
+///   have : (↑(0 : I32) : Int) = 0 := by rfl
+///   split at h_returns <;> simp_all
 /// proof (h2):
 ///   unfold abs at h_returns
-///   split at h_returns <;> intros <;> (try cases h_req) <;> (try have := Aeneas.Std.IScalar.hmin x) <;> (try have := Aeneas.Std.IScalar.hmax x) <;> (try have : (↑(0 : I32) : Int) = 0 := by rfl) <;> (try have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)) <;> (try split at h_bound) <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg, Aeneas.Std.IScalar.inBounds]) <;> scalar_tac
+///   have : (↑(0 : I32) : Int) = 0 := by rfl
+///   have := Aeneas.Std.IScalar.hmin x
+///   have := Aeneas.Std.IScalar.hmax x
+///   split at h_returns
+///   · have h_bound := Aeneas.Std.IScalar.tryMk_eq IScalarTy.I32 (-↑x)
+///     split at h_bound <;> (try simp_all [HNeg.hNeg, Aeneas.Std.IScalar.neg])
+///   · simp_all
 /// ```
 pub unsafe fn abs(x: i32) -> i32 {
     if x < 0 { -x } else { x }