fact: Fixpoint and_with_bit (a: list _lit) (bt: _lit) : list carry := match a with | nil => nil | ai :: a' => (Cand (Clit bt) (Clit ai)) :: and_with_bit a' bt end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance