fact: Fixpoint and_with_bool (a: list bool) (bt: bool) : list bool := match a with | nil => nil | ai :: a' => (bt && ai) :: and_with_bool a' bt end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance