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