Change `|-i` to take `psis` instead of a `sigma`
The new judgement should look something like:
|-i psis; args ~> Theta ;<Q>; <| exp ; phi |>
As is appearent, instead of taking sigmas, and then returning a rho, we are giving |-i some psis -- that were synthesized using the visible arity of args -- and then not returning any rhos!
This is because we already got the rho when we splitted the sigma at the call-site:
|-arity args ~> nva
|-split nva; sigma ~> psis, rho -- psis includes invisible ones (as now)
|-i psis; args ~> Theta, Qs, <exp,phi>
Theta(rho)
....
------------- INST-CHECK