-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.ā§.