proposition: Lemma bv_eq_reflect n (a b: bitvector n) : bv_eq a b = true <-> a = b.
proof: Proof. unfold bv_eq. rewrite M.bv_eq_reflect. split. - revert a b. intros [a Ha] [b Hb]. simpl. intros ->. rewrite (proof_irrelevance _ Ha Hb). reflexivity. - intros. case a in *. case b in *. simpl in *. now inversion H. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance