proposition: Lemma case_first_value : forall (E : Set) (x y : E) (d : data) (q : queue data), first data q = value data d -> match q with | empty => x | input _ _ => y end = y.
proof: Proof. intro; intro; intro; intro; intro. elim q. simpl in |- *. intuition. discriminate. intros d0 q0 H H0. trivial. Qed.
imports: bibli