proposition: Theorem parse_complete : forall l:list par, wp l -> parse nil L l <> None.
proof: Proof. intros l H; replace l with (l ++ nil). red in |- *; intros H'. assert (e : parse nil L nil = None). - apply parse_complete_aux with (2 := H'); auto. apply wp_imp_wp'; auto. - discriminate. - rewrite <- app_nil_r; auto. Qed.
imports: List Arith