proposition: Lemma Vtrue_break : forall n1 n2 (bs : bools (n1+n2)), Vtrue (fst (Vbreak bs)) + Vtrue (snd (Vbreak bs)) = Vtrue bs.
proof: Proof. induction n1; simpl; intros. refl. VSntac bs. simpl. case (Vhead bs); simpl. f_equal. apply IHn1. apply IHn1. Qed.
imports: CoLoR(VecUtil LogicUtil)