let dummy = C.Sort C.Prop in
(*CSC: to be moved in cicSubstitution? *)
let rec subst_inductive_type_with_dummy _ = function
+ | C.Meta (_,(_,C.Irl _)) as x -> x
+ | C.Meta (i,(lift,C.Ctx ls)) ->
+ C.Meta (i,(lift,C.Ctx
+ (List.map (subst_inductive_type_with_dummy ()) ls)))
| C.Const (Ref.Ref (uri',Ref.Ind (true,0,_))) when NUri.eq uri' uri -> dummy
| C.Appl ((C.Const (Ref.Ref (uri',Ref.Ind (true,0,lno))))::tl)
when NUri.eq uri' uri ->