proposition: Lemma not_empty_implies_last : forall (E : Set) (q : queue E), q <> empty E -> exists x : E, first E q = value E x.
proof: Proof. intro. simple induction q. auto. intros. elim H; auto. intros d q0. case q0. simpl in |- *. intros. split with d. auto. simpl in |- *. intros. apply H. discriminate. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8