proposition: Theorem parse_complete_aux : forall l:list par, wp' l -> forall (s:list bin) (t:bin) (l':list par), parse s t (l ++ l') = None -> forall (s':list bin) (t':bin), length s' = length s -> parse s' t' l' = None.
proof: Proof. simple induction 1. - simpl; intros; eapply parse_reject_indep_t; eauto. - intros l1 l2 Hp1 Hr1 Hp2 Hr2 s t l' Hrej s' t' Hle. apply Hr2 with (s := s') (t := N t L). change (parse (t :: s') L (close :: l2 ++ l') = None) in |- *. simpl in Hrej. rewrite <- app_assoc in Hrej. apply Hr1 with (1 := Hrej). simpl; auto with arith. auto. Qed.
imports: List Arith