-@IH -IH /3 width=3 by rsx_lpxs_trans, rsx_rdeq_trans/ -HL1 #K2 #HLK2 #HnLK2
-lapply (rdeq_rdneq_trans ā¦ HL02 ā¦ HnLK2) -HnLK2 #H
-elim (rdeq_lpxs_trans ā¦ HLK2 ā¦ HL02) -L2 #K0 #HLK0 #HK02
-lapply (rdneq_rdeq_canc_dx ā¦ H ā¦ HK02) -H #HnLK0
-elim (rdeq_dec L1 L0 T) #H
-[ lapply (rdeq_rdneq_trans ā¦ H ā¦ HnLK0) -H -HnLK0 #Hn10
+@IH -IH /3 width=3 by rsx_lpxs_trans, rsx_reqx_trans/ -HL1 #K2 #HLK2 #HnLK2
+lapply (reqx_rneqx_trans ā¦ HL02 ā¦ HnLK2) -HnLK2 #H
+elim (reqx_lpxs_trans ā¦ HLK2 ā¦ HL02) -L2 #K0 #HLK0 #HK02
+lapply (rneqx_reqx_canc_dx ā¦ H ā¦ HK02) -H #HnLK0
+elim (reqx_dec L1 L0 T) #H
+[ lapply (reqx_rneqx_trans ā¦ H ā¦ HnLK0) -H -HnLK0 #Hn10