proposition: Lemma first_out_input : forall (d0 d1 : data) (q : queue data), first_out data (input data d0 (input data d1 q)) = input data d0 (first_out data (input data d1 q)).
proof: Proof. intros d0 d1 q. unfold first_out in |- *. auto. Qed.
imports: bibli