proposition: Lemma input_S_card : forall (d d' : data) (q : queue data), d = d' -> card data eq_data_dec d (input data d' q) = (card data eq_data_dec d q + 1)%Z.
proof: Proof. intros; simpl in |- *. rewrite H; rewrite case_eq; trivial. Qed.
imports: bibli