proposition: Lemma input_diff_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.
proof: Proof. intros; simpl in |- *. rewrite case_ineq; trivial. Qed.
imports: bibli