proposition: Lemma prop_and_with_bit: forall a b, map interp_carry (and_with_bit a b) = RAWBITVECTOR_LIST.and_with_bool (map (Lit.interp rho) a) (Lit.interp rho b).
proof: Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. now simpl in *. - intros. simpl in *. now rewrite IHa. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance