proposition: Lemma not_in_q_shuffle : forall (m1 m2 : data) (q1 q2 q3 q4 : queue data), ~ In_queue data m2 (append data q1 (input data m1 q2)) -> append data q1 q2 = append data q3 q4 -> ~ In_queue data m2 (append data q3 (input data m1 q4)).
proof: Proof. intros m1 m2 q1 q2 q3 q4 H H0. apply not_in_q_shuffle1. simpl in |- *. rewrite <- H0. unfold not in |- *; intro. elim H. apply in_q_shuffle1. simpl in |- *. auto. Qed.
imports: bibli