proposition: Theorem parse_invert : forall (l:list par) (t:bin), parse nil L l = Some t -> bin_to_string' t = l.
proof: Proof. intros; replace l with (unparse_stack nil ++ bin_to_string' L ++ l); auto. apply parse_invert_aux; auto. Qed.
imports: List Arith