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