proposition: Lemma Vtrue_cast : forall n (bs : bools n) p (h:n=p), Vtrue (Vcast bs h) = Vtrue bs.
proof: Proof. induction bs; induction p; intros. rewrite Vcast_refl. refl. discr. discr. rewrite Vcast_cons. simpl. case h. f_equal. apply IHbs. apply IHbs. Qed.
imports: CoLoR(VecUtil LogicUtil)