proposition: Lemma bv_and_assoc: forall n a b c, size a = n -> size b = n -> size c = n -> (bv_and a (bv_and b c)) = (bv_and (bv_and a b) c).
proof: Proof. intros n a b c H0 H1 H2. unfold bv_and, size, bits in *. rewrite H1, H2. rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite N.compare_refl. rewrite N.eqb_compare. rewrite N.eqb_compare. rewrite H0. rewrite N.compare_refl. rewrite <- (@map2_and_length a b). rewrite <- map2_and_length. rewrite H0, H1. rewrite N.compare_refl. rewrite map2_and_assoc; reflexivity. now rewrite <- Nat2N.inj_iff, H1. now rewrite <- Nat2N.inj_iff, H0. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance