fact: Fixpoint extract (x: list bool) (i j: nat) : list bool := match x with | [] => [] | bx :: x' => match i with | O => match j with | O => [] | S j' => bx :: extract x' i j' end | S i' => match j with | O => [] | S j' => extract x' i' j' end end end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance