E[G] |- t : T c Ï EÈ G |
WF(E;Def(G)(c:=t:T))[G] |
WF(E;Def(G)(c:=t:T); F)[D] |
WF(E; F{c/t})[D{c/t}] |
WF(E; Def(G::(x:U))(c:=t:T); F)[D] WF(E)[G] |
WF(E;Def(G)(c:=[x:U]t:(x:U)T); F{c/(c x)})[D{c/(c x)}] |
WF(E; Def(D)(c:=t:T))[G] |
WF(E;Def(D)(c:=t:T))[D] |