proposition: Theorem recognize_sound_aux : forall (l:list par) (n:nat), recognize n l = true -> wp (make_list _ open n ++ l).
proof: Proof. simple induction l; simpl. - intros n; case n. simpl ; intros; apply wp_nil. intros n' H; discriminate H. - intros a; case a; simpl ; clear a. + intros l' H n H0. rewrite <- make_list_end; auto. + intros l' H n; case n; clear n. intros H'; discriminate H'. intros n H0; rewrite make_list_end; apply wp_remove_oc;auto. Qed.
imports: List Arith