diff options
Diffstat (limited to 'theories/Bool/Bvector.v')
| -rw-r--r-- | theories/Bool/Bvector.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 0cb3c3670..88bc15c69 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -92,7 +92,7 @@ Proof. exact (Vcons a 0 v). inversion v as [| a0 n0 H0 H1 ]. - exact (Vcons a (S n) (f a H0)). + exact (Vcons a0 (S n) (f a H0)). Defined. Lemma Vshiftrepeat : forall n:nat, vector (S n) -> vector (S (S n)). |