proposition: Lemma eq_rec: forall (n: N) (a b: BITVECTOR_LIST.bitvector n), BITVECTOR_LIST.bv a = BITVECTOR_LIST.bv b -> a = b.
proof: Proof. intros. destruct a, b. unfold BITVECTOR_LIST.bv in H. revert wf0. rewrite H. intros. now rewrite (proof_irrelevance _ wf0 wf1). Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance