This is the request for references.
It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent.
It is also know that there is a double-negation Godel-Gentzen translation from classical logic to intuitionistic. (So we can prove something in IZF.)
Does exist a similar result about CIC with axiom of choice? By CIC I mean the Calculus of Inductive Constructions, the system which The Coq proof assistant is based on.
Does exist a model of CIC+choice inside CIC? Where can I learn about it?
Definition choice :=
forall (A B : Type) (P : A -> B -> Prop),
(forall a : A, exists b : B, P a b) ->
exists f : A -> B, forall a : A, P a (f a).