proposition: Lemma bv_eq_reflect a b : bv_eq a b = true <-> a = b.
proof: Proof. unfold bv_eq. case_eq (size a =? size b)%N; intro Heq; simpl. - apply List_eq. - split; try discriminate. intro H. rewrite H, N.eqb_refl in Heq. discriminate. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance