proposition: Theorem recognize_complete_aux : forall l:list par, wp l -> forall (n:nat) (l':list par), recognize n (l ++ l') = recognize n l'.
proof: Proof. intros l H; elim H. - simpl; auto. - intros l1 l2 H1 Hrec1 H2 Hrec2 n l'. rewrite <- app_assoc; transitivity (recognize n (l2 ++ l')); auto. - intros l1 H1 Hrec n l'; simpl ; rewrite <- app_assoc; rewrite Hrec; simpl ; auto. Qed.
imports: List Arith