proposition: Lemma prop_and_with_bit2: forall bs1 b, length (and_with_bit bs1 b) = length bs1.
proof: Proof. intros bs1. induction bs1. - intros. now simpl. - intros. simpl. now rewrite IHbs1. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance