proposition: Lemma Forall_shiftin A: forall (P : A -> Prop) a n (v : t A n), Forall P (shiftin a v) <-> (P a /\ Forall P v).
proof: Proof. intros P a n v. induction v as [|b n v IH]. - apply Forall_cons_iff. - cbn. rewrite !Forall_cons_iff. tauto. Qed.
imports: VectorDef PeanoNat Eqdep_dec