proposition: Lemma bitOf_of_bits: forall l (a: BITVECTOR_LIST.bitvector (N.of_nat (length l))), (forall i, (i < (length l))%nat -> nth i l false = (@BITVECTOR_LIST.bitOf (N.of_nat (length l)) i a)) -> (BITVECTOR_LIST.bv_eq a (BITVECTOR_LIST.of_bits l)).
proof: Proof. intros l a H. unfold BITVECTOR_LIST.of_bits in *. unfold BITVECTOR_LIST.bitOf in *. unfold BITVECTOR_LIST.bv_eq, BITVECTOR_LIST.bv in *. unfold RAWBITVECTOR_LIST.bitOf in *. destruct a. unfold RAWBITVECTOR_LIST.of_bits. unfold RAWBITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST.bits in *. rewrite wf0. rewrite N.eqb_compare. rewrite N.compare_refl. cut (Datatypes.length l = Datatypes.length bv). intro wf1. apply (@nth_eq l bv wf1) in H. rewrite H. unfold RAWBITVECTOR_LIST.bv_eq, RAWBITVECTOR_LIST.size, RAWBITVECTOR_LIST.bits in *. rewrite RAWBITVECTOR_LIST.List_eq_refl; auto with smtcoq_core. apply inj_iff in wf0. now do 2 rewrite id' in wf0. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance