proposition: Lemma Vtrue_app : forall n1 (bs1 : bools n1) n2 (bs2 : bools n2), Vtrue (Vapp bs1 bs2) = Vtrue bs1 + Vtrue bs2.
proof: Proof. induction bs1; simpl. auto. intros. ded (IHbs1 n2 bs2). rewrite H. case h; refl. Qed.
imports: CoLoR(VecUtil LogicUtil)