proposition: Theorem wp_remove_oc_aux : forall l:list par, wp l -> forall l1 l2:list par, l1 ++ l2 = l -> wp (l1 ++ open :: close :: l2).
proof: Proof. intros l H; elim H. - intros l1 l2 H1; elim (app_eq_nil _ _ H1); auto. simpl in |- *; intros Heq1 Heq2; rewrite Heq1; rewrite Heq2; apply wp_oc. - intros l1 l2 Hp1 Hr1 Hp2 Hr2 l3 l4 Heq. elim app_decompose with (1 := Heq). intros [l1' [Heq1 Heq2]]; rewrite Heq1, <- app_assoc; apply wp_concat; auto. intros [a' [l2' [Heq1 Heq2]]]. rewrite Heq2. repeat rewrite app_comm_cons. rewrite app_assoc. apply wp_concat; auto. - idtac. intros l' Hp'' Hrec l1; case l1. simpl ; intros l2 Heq; rewrite Heq. change (wp (open :: nil ++ close :: open :: l' ++ close :: nil)); auto. simpl; intros c l1' l2; case l2. + intros Heq; injection Heq; intros Heq1 Heq2. rewrite app_nil_r in Heq1; rewrite Heq1; rewrite Heq2. rewrite app_comm_cons. apply wp_concat; auto. + intros c' l2'; elim (cons_to_app_end l2' c'). intros c'' [l2'' Heq]; rewrite Heq. rewrite app_assoc; intros Heq1. injection Heq1; intros Heq2 Heq3; elim last_same with (1 := Heq2). intros Heq4 Heq5; rewrite Heq5; rewrite Heq3. change (wp (open :: l1' ++ (open :: close :: l2'') ++ close :: nil)) . rewrite app_assoc; auto. Qed.
imports: List Arith