proposition: Lemma prop_checkbb': forall (a: int) (bs: list _lit), (check_bb a bs 0 (length bs) = true) -> (forall i0, (i0 < (length bs) )%nat -> (Lit.interp rho (nth i0 bs 1)) = (@BITVECTOR_LIST.bitOf (N.of_nat(length bs)) i0 (interp_form_hatom_bv a (N.of_nat (length bs))))).
proof: Proof. intros. specialize (@prop_checkbb a bs 0 (length bs)). intros Hp. cut ((i0 - 0)%nat = i0%nat). intro Hc. cut (Datatypes.length bs = (Datatypes.length bs - 0)%nat). intro Hc2. specialize (@Hp Hc2 H i0). cut ( (0 <= i0 < Datatypes.length bs)%nat). intro Hc3. specialize (@Hp Hc3). now rewrite Hc in Hp. lia. lia. lia. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance