proposition: Lemma beq_vec_ok_in1 : forall n (v : vector A n) (hyp : forall x, Vin x v -> forall y, beq x y = true <-> x = y) p (w : vector A p) (h : beq_vec beq v w = true), Vcast v (beq_vec_ok_length A beq h) = w.
proof: Proof. induction v; destruct w; intro; try discr. rewrite Vcast_refl; refl. generalize (beq_vec_ok_length A beq h1); intros e. simpl in h1; destruct (andb_elim h1). assert (ha : Vin h (Vcons h v)). simpl. auto. ded (hyp _ ha h0). rewrite H1 in H. subst h0. rewrite Vcast_cons. assert (hyp' : forall x, Vin x v -> forall y, beq x y = true <-> x=y). intros x hx. apply hyp. simpl. auto. destruct (andb_elim h1). ded (IHv hyp' _ w H2). rewrite <- H3. f_equal; apply Vcast_pi. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)