proposition: Lemma Id_is_bijective : forall A : Setoid, bijective (Id A).
proof: Proof. intros A; red in |- *. split; [ red in |- * | idtac ]. simpl in |- *; auto with algebra. red in |- *. intros y; exists y; try assumption; auto with algebra. Qed.