proposition: Lemma beq_vec_ok_in2 : forall n (v : vector A n) (hyp : forall x, Vin x v -> forall y, beq x y = true <-> x = y) w, v = w -> beq_vec beq v w = true.
proof: Proof. induction v; intros. VOtac. refl. VSntac w. rewrite H0 in H. Veqtac. subst h. simpl. apply andb_intro. set (a := Vhead w). assert (Vin a (Vcons a v)). simpl. auto. ded (hyp _ H a). rewrite H1. refl. apply IHv. intros. apply hyp. simpl. auto. exact H3. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)