proposition: Lemma bv_mk_eq l1 l2 : bv_eq l1 l2 = beq_list l1 l2.
proof: Proof. unfold bv_eq, size, bits. case_eq (Nat.eqb (length l1) (length l2)); intro Heq. - now rewrite (EqNat.beq_nat_true _ _ Heq), N.eqb_refl. - replace (N.of_nat (length l1) =? N.of_nat (length l2)) with false. * revert l2 Heq. induction l1 as [ |b1 l1 IHl1]; intros [ |b2 l2]; simpl in *; auto. intro Heq. now rewrite <- (IHl1 _ Heq), andb_false_r. * symmetry. rewrite N.eqb_neq. intro H. apply Nat2N.inj in H. rewrite H in Heq. rewrite <- EqNat.beq_nat_refl in Heq. discriminate. Qed.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance