fact: Fixpoint check_extract2 (x bsres: list _lit) (i j: nat) : bool := match x with | [] => match bsres with [] => true | _ => false end | bx :: x' => match i with | O => match j, bsres with | O, nil => true | S j', b :: bsres' => (bx =? b) && check_extract2 x' bsres' i j' | _, _ => false end | S i' => match j, bsres with | O, nil => true | S j', _ => check_extract2 x' bsres i' j' | _, _ => false 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