fact: Fixpoint beq_list (l m : list bool) {struct l} := match l, m with | nil, nil => true | x :: l', y :: m' => (Bool.eqb x y) && (beq_list l' m') | _, _ => false end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance