proposition: Lemma in_q_shuffle1 : forall (m1 m2 : data) (q3 q4 : queue data), In_queue data m2 (input data m1 (append data q3 q4)) -> In_queue data m2 (append data q3 (input data m1 q4)).
proof: Proof. intros m1 m2 q3 q4 H. apply inqueue_append. simpl in |- *. generalize H; simpl in |- *; intro. elim H0; intro. auto. generalize H1. elim q3. simpl in |- *. intro H2. auto. simpl in |- *. intros d q H2 H3. elim H3; intro. auto. generalize (H2 H4); intro. elim H5; intro; auto. Qed.
imports: bibli