fact: Definition sextend_lit (x: list _lit) (i: nat): list _lit := match x with | [] => mk_list_lit_false i | xb :: x' => extend_lit x i xb end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance