From c49f18c94aae676830ed9c52632b4af6d814d566 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Mon, 30 Oct 2023 14:12:09 +0100 Subject: [PATCH] Update --- src/subsequences.v | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 6581880..e659f0b 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -125,10 +125,6 @@ Proof. Qed. - - - - Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type), subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2. Proof. @@ -171,7 +167,6 @@ Qed. *) - Theorem subsequence2_dec : (forall x y : Type, {x = y} + {x <> y}) -> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.