Adding a proof of eta on Vector.t of non-zero size.

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] *)