fact: Fixpoint _list2nat_be (a: list bool) (n i: nat) : nat := match a with | [] => n | xa :: xsa => if xa then _list2nat_be xsa (n + (pow2 i)) (i + 1) else _list2nat_be xsa n (i + 1) end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance