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 }.