proposition: Lemma Vconseq : forall (a:A)(n m:nat), n = m -> forall (v:t A n)(w:t A m), JMeq v w -> JMeq (cons A a n v)(cons A a m w).
proof: Proof. intros a n m Heq; rewrite Heq. intros v w HJeq. rewrite HJeq; reflexivity. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector