| NCic.LetIn (n,ty_s,s,t) ->
Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t)
| NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop
| NCic.LetIn (n,ty_s,s,t) ->
Cic.LetIn (nn_2_on n,convert_term k s,convert_term k ty_s, convert_term (k+1) t)
| NCic.Sort NCic.Prop -> Cic.Sort Cic.Prop