-(* FG: We do not discharge the nsubst here ?? *)
- let args = get_args st u in
- if args = [] then C.Rel (discharge st u) else
- let s = List.map (mk_arg s) args in
- (* C.Appl ( *) C.Rel (discharge st u) (* :: discharge_nsubst st s) *)
+(* We do not discharge the nsubst because variables are not closed *)
+(* thus only the identity nsubst should be allowed *)
+ if s <> [] then assert false else
+ C.Rel (discharge st u)