proposition: Lemma In_shiftin A: forall a b n (v : t A n), In a (shiftin b v) <-> (b = a \/ In a v).
proof: Proof. intros a b n v. induction v as [|c n v IH]. - apply In_cons_iff. - cbn. rewrite !In_cons_iff. tauto. Qed.
imports: VectorDef PeanoNat Eqdep_dec