proposition: Theorem parse_rel_sound_aux : forall (l1 l2:list par) (t:bin), parse_rel l1 l2 t -> l1 = bin_to_string t ++ l2.
proof: Proof. intros l1 l2 t H; elim H; clear H l1 l2 t. - intros l1 l2 l3 t1 t2 Hp Hr1 Hp2 Hr2; simpl. rewrite <- app_assoc, Hr1; simpl. now rewrite Hr2. - reflexivity. - reflexivity. Qed.
imports: List Arith