diff options
Diffstat (limited to 'theories/Vectors')
-rw-r--r-- | theories/Vectors/VectorSpec.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 7f4228dd6..46b537737 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -22,6 +22,16 @@ Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n} with | eq_refl => conj eq_refl eq_refl end. +Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v. +Proof. + change + (match S n with + | 0 => fun v : t A 0 => v = v + | S n => fun v => v = hd v :: tl v + end v). + destruct v; reflexivity. +Defined. + (** Lemmas are done for functions that use [Fin.t] but thanks to [Peano_dec.le_unique], all is true for the one that use [lt] *) |