proposition: Lemma prop_interp_carry3: forall bs2, map interp_carry (lit_to_carry bs2) = map (Lit.interp rho) bs2.
proof: Proof. intro bs2. induction bs2 as [ | xbs2 xsbs2 IHbs2 ]. - now simpl. - simpl. now rewrite IHbs2. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance