proposition: Lemma Vin_cast_elim : forall m n (H : m=n) (v : vector A m) x, Vin x (Vcast v H) -> Vin x v.
proof: Proof. intros m n H. case H. intros v x. rewrite Vcast_refl. auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)