proposition: Lemma Forall_rev A: forall (P : A -> Prop) n (v : t A n), Forall P (rev v) <-> Forall P v.
proof: Proof. intros P n v. induction v as [|a n v IH]. - now rewrite rev_nil. - now rewrite rev_cons, Forall_shiftin, Forall_cons_iff, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec