proposition: Lemma bv_or_comm: forall n a b, (size a) = n -> (size b) = n -> bv_or a b = bv_or b a.
proof: Proof. intros a b n H0 H1. unfold bv_or. rewrite H0, H1. rewrite N.eqb_compare. rewrite N.compare_refl. rewrite map2_or_comm. reflexivity. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance