I can now create a list of terms simply if types are in the context
More progresses. Need a generalization of lsubst?