-lemma rsx_inv_bind_void (h) (G):
- āp,I,L,V,T. G ā¢ ā¬*[h,ā[p,I]V.T] šāŖLā« ā
- ā§ā§ G ā¢ ā¬*[h,V] šāŖLā« & G ā¢ ā¬*[h,T] šāŖL.ā§ā«.
+lemma rsx_inv_bind_void (G):
+ āp,I,L,V,T. G ā¢ ā¬*š[ā[p,I]V.T] L ā
+ ā§ā§ G ā¢ ā¬*š[V] L & G ā¢ ā¬*š[T] L.ā§.