-lemma rsx_fwd_lref_pair_drops (h) (G):
- āL,i. G ā¢ ā¬*š[h,#i] L ā
- āI,K,V. ā©[i] L ā K.ā[I]V ā G ā¢ ā¬*š[h,V] K.
-#h #G #L #i #HL #I #K #V #HLK
+lemma rsx_fwd_lref_pair_drops (G):
+ āL,i. G ā¢ ā¬*š[#i] L ā
+ āI,K,V. ā©[i] L ā K.ā[I]V ā G ā¢ ā¬*š[V] K.
+#G #L #i #HL #I #K #V #HLK