[TYPES] independence of AC! or AC from CIC

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear all

is it known whether the axiom of unique choice  (AC!)  or even
the only axiom of choice (both as formulas in Prop)

are independent from the Calculus of Inductive Constructions ?

Any reference?

For the pure Calculus of Constructions the  independence of AC! and AC 
was shown
in
T. Streicher " Independence of the induction principle and the axiom of 
choice in the pure calculus of constructions." TCS, 1992, vol.103.

Many thanks for your cooperation
Milly
(Maria Emilia Maietti)