- Equality of meanings:
-
[[fun I = E in ...: theta]
= [[define I(I:tauexp) = ...
in invoke
I(E): theta]]
-
[[fun I = E in ...: theta]
= [[pi |- ...: theta]](
-U- {I=[[pi |- E: tauexp]]})
where pi = pi -U- {I:tauexp}
-
[[define I(I:tauexp) = ...in invoke
I(E): theta]]
= [[pi |- invoke I(E): theta]]
where pi = pi -U- {I: tauexp
theta},
and e = -U- {I=}
and = [[pi -U- ...: theta]](
-U- {I=})
= where = [[pi |- E:
tauexp]]
= [[pi |- ...: theta]]( -U- {I=})
= [[pi |- ...: theta]]( -U- {I=})
where = [[pi|- E: tauexp]]
(since I does not appear in E)
Proof adapts to eager evaluation as well.