From 6ab9bda4af68093ae8ec680b86031bd9abf91439 Mon Sep 17 00:00:00 2001
From: dnezam <55559979+dnezam@users.noreply.github.com>
Date: Thu, 8 Feb 2024 11:35:02 +0100
Subject: [PATCH] Update comment

---
 seqs/seqs.gobra | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/seqs/seqs.gobra b/seqs/seqs.gobra
index e8372ed..4ee8d6a 100644
--- a/seqs/seqs.gobra
+++ b/seqs/seqs.gobra
@@ -407,9 +407,9 @@ ghost
 ensures Flatten(seq[seq[int]]{xs}) == xs
 decreases
 pure func FlattenSingleton(xs seq[int]) util.Unit {
-	// This manually asserts the body of Flatten. For more information, see
-	// https://github.com/viperproject/silicon/issues/803
-	return util.Asserting(Flatten(seq[seq[int]]{xs}) == seq[seq[int]]{xs}[0] ++ Flatten(seq[seq[int]]{xs}[1:]))
+	// See https://github.com/viperproject/silicon/issues/803 for an explanation
+	// of this proof.
+	return util.Asserting(Flatten(seq[seq[int]]{xs}[1:]) == Empty())
 }
 
 // The length of a flattened sequence of sequences xs is greater than or equal