fact: Fixpoint lit_to_carry (bs: list _lit) : list carry := match bs with | nil => [] | xbs :: xsbs => Clit xbs :: lit_to_carry xsbs end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance