-lemma rdsx_fwd_bind_dx (h) (o) (G):
- āp,I,L,V,T. G ā¢ ā¬*[h, o, ā{p,I}V.T] šā¦Lā¦ ā
- G ā¢ ā¬*[h, o, T] šā¦L.ā§ā¦.
-#h #o #G #p #I #L #V #T #H
+lemma rdsx_fwd_bind_dx (h) (G):
+ āp,I,L,V,T. G ā¢ ā¬*[h,ā{p,I}V.T] šā¦Lā¦ ā
+ G ā¢ ā¬*[h,T] šā¦L.ā§ā¦.
+#h #G #p #I #L #V #T #H