-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.โง.