fact: Fixpoint parse (s:list bin) (t:bin) (l:list par) {struct l} : option bin := match l with | nil => match s with | nil => Some t | _ => None (A:=bin) end | open :: l' => parse (t :: s) L l' | close :: l' => match s with | t' :: s' => parse s' (N t' t) l' | _ => None (A:=bin) end end.
imports: List Arith