proposition: Lemma case_append_right : forall (E : Set) (x y : E) (q1 q2 : queue data) (d : data), match append q1 (input data d q2) with | empty => x | input _ _ => y end = y.
proof: Proof. intros E x y q1 q2 d. elim q1. simpl in |- *. trivial. intros d0 q H. rewrite <- (input_append d0 q (input data d q2)). trivial. Qed.
imports: bibli