Partial theory instantiation

[disteph]

Just to record it on github:

a: theory
begin

  t : type
  t2 : type
  
  interface : [ t -> setof[t2]]

end a

b: theory
begin

  t2 : type = { v1, v2 }

  importing a{{ t2     := t2,
                interface   := lambda (R : t) : lambda (i : t2) : true }}
  
end b

is supposed to type-check, unless I'm mistaken, even though t is not instantiated.