proposition: Theorem wp'_concat : forall l1 l2:list par, wp' l1 -> wp' l2 -> wp' (l1 ++ l2).
proof: Proof. intros l1 l2 H; generalize l2; clear l2. elim H. - simpl; auto. - intros l1' l2' Hb1' Hr1 Hb2' Hr2 l2 Hb2; simpl; rewrite <- app_assoc. simpl; apply wp'_cons; auto. Qed.
imports: List Arith