let rec aux m_subst subst ctx = function
| (i,(tag,[],ty)) :: tl ->
let name = "x" ^ string_of_int (List.length ctx) in
let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in
let rec aux m_subst subst ctx = function
| (i,(tag,[],ty)) :: tl ->
let name = "x" ^ string_of_int (List.length ctx) in
let subst = (i,(tag,[],NCic.Rel (List.length tl+1),ty))::subst in