From e748e26915a4a1fe93be22ead99caa20915b9f41 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 30 Oct 2023 17:11:08 +0100 Subject: [PATCH] Update --- src/subsequences.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/subsequences.v b/src/subsequences.v index 9a65c7c..52482d8 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -289,3 +289,7 @@ Qed. Example test3: subsequence [1;2;3;4;5] [1;3;5]. Proof. rewrite subsequence_eq_def. + exists [true; false; true; false; true]. + split; reflexivity. + apply Nat.eq_dec. +Qed.