fact: Definition lit_of_bool (b: bool) :_lit := if (Bool.eqb b true) then Lit._true else Lit._false.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance