proposition: Theorem parse_rel_sound : forall l:list par, (exists t : bin, parse_rel l nil t) -> wp l.
proof: Proof. intros l [t H]; replace l with (bin_to_string t). - apply bin_to_string_wp. - symmetry; replace (bin_to_string t) with (bin_to_string t ++ nil). + apply parse_rel_sound_aux; auto. + rewrite app_nil_r; auto. Qed.
imports: List Arith