fact: Fixpoint extend_lit (x: list _lit) (i: nat) (b: _lit) {struct i}: list _lit := match i with | O => x | S i' => b :: extend_lit x i' b end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance