Update
This commit is contained in:
parent
81f0311165
commit
c49f18c94a
|
@ -125,10 +125,6 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
|
Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
|
||||||
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
|
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
|
||||||
Proof.
|
Proof.
|
||||||
|
@ -171,7 +167,6 @@ Qed.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_dec :
|
Theorem subsequence2_dec :
|
||||||
(forall x y : Type, {x = y} + {x <> y})
|
(forall x y : Type, {x = y} + {x <> y})
|
||||||
-> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
|
-> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
|
||||||
|
|
Loading…
Reference in New Issue
Block a user