fact: Fixpoint mkzeros (k: nat) : list carry := match k with | O => nil | S k => (Clit Lit._false) :: mkzeros k end .
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance