proposition: Lemma of_list_to_list_opp A n (v: t A n): rew length_to_list _ _ _ in of_list (to_list v) = v.
proof: Proof. induction v as [ | h n v IHv ]. - now apply case0 with (P := fun v => v = nil A). - replace (length_to_list _ _ (cons _ h _ v)) with (f_equal S (length_to_list _ _ v)) by apply (UIP_dec Nat.eq_dec). cbn; rewrite map_subst_map. f_equal. now etransitivity; [ | apply IHv]. Qed.
imports: VectorDef PeanoNat Eqdep_dec