proposition: Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, vector_nth i v1 = Some a -> vector_nth i v2 = Some b -> vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
proof: Proof. intros n v1 v2; pattern n,v1,v2. apply vector_double_rect. simpl. destruct i; discriminate 1. destruct i; simpl;auto. injection 1; injection 2;intros; subst a; subst b; auto. Qed.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat Bool