fact: Fixpoint mk_list_lit_false (t: nat) : list _lit := match t with | O => [] | S t' => Lit._false :: (mk_list_lit_false t') end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance