fact: Fixpoint recognize (n:nat) (l:list par) {struct l} : bool := match l with | nil => match n with | O => true | _ => false end | open :: l' => recognize (S n) l' | close :: l' => match n with | O => false | S n' => recognize n' l' end end.
imports: List Arith