proposition: Lemma rev_cons A: forall a n (v : t A n), rev (a :: v) = shiftin a (rev v).
proof: Proof. intros a n v. unfold rev, rev_append, eq_rect_r. rewrite !rew_compose. enough (H : forall m (w : t A m) k (E1 : _ = k) E2, rew [t A] E2 in rev_append_tail v (shiftin a w) = shiftin a (rew [t A] E1 in rev_append_tail v w)) by apply (H 0 []). induction v as [|b n v IH]; intros m w k E1 E2; cbn. - subst k. now rewrite (UIP_refl_nat _ E2). - apply (IH _ (b :: w)). Qed.
imports: VectorDef PeanoNat Eqdep_dec