vec_rev_involutive.v

Require Import Coq.Lists.List Coq.Logic.Eqdep.
Definition vec (A: Type) (n: nat) : Type := {l: list A | length l = n}.

Section vec_rev.
  Variable A : Type.
  Variable n : nat.

  Definition vec_rev (l: vec A n): vec A n.
  Proof.
    refine (exist _ (rev (proj1_sig l)) _).
    destruct l; rewrite rev_length; trivial.
  Defined.

  Lemma vec_rev_involutive: forall l, vec_rev (vec_rev l) = l.
  Proof.
    intro; unshelve eapply eq_sig.
    - apply rev_involutive.
    - apply UIP.
  Qed.
End vec_rev.