fact: Fixpoint beq_listP (l m : list bool) {struct l} := match l, m with | nil, nil => True | x :: l', y :: m' => (x = y) /\ (beq_listP l' m') | _, _ => False end.
imports: List Bool NArith Psatz Int63 Nnat ZArith Misc ProofIrrelevance