concise rev_cons

Author: mrhaandi

theories/Vectors/VectorSpec.v

@@ -545,16 +545,6 @@ intros P a n v. induction v as [|b n v IH].
 - cbn. rewrite !Forall_cons_iff. tauto.
 Qed.
 
-Lemma rev_append_tail_shiftin A : forall a n (v : t A n) m (w : t A m) k
-  (E1 : Nat.tail_add n m = k) (E2 : Nat.tail_add n (S m) = S k),
-    rew [t A] E2 in rev_append_tail v (shiftin a w) =
-    shiftin a (rew [t A] E1 in rev_append_tail v w).
-Proof.
-intros a n v. 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.
-
 (** ** Properties of [rev] *)
 
 Lemma rev_nil A: rev (nil A) = [].
@@ -567,7 +557,12 @@ Lemma rev_cons A: forall a n (v : t A n), rev (a :: v) = shiftin a (rev v).
 Proof.
 intros a n v. unfold rev, rev_append, eq_rect_r.
 rewrite !rew_compose.
-apply (rev_append_tail_shiftin A a n v 0 []).
+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.
 
 Lemma rev_shiftin A: forall a n (v : t A n),