- elim (lpxs_rneqx_inv_step_sn … H10 … Hn10) -H10 -Hn10
- /3 width=8 by reqx_trans/
-| elim (lpxs_rneqx_inv_step_sn … HL10 … H) -HL10 -H #L #K #HL1 #HnL1 #HLK #HKL0
- elim (reqx_lpxs_trans … HLK0 … HKL0) -L0
- /3 width=8 by lpxs_trans, reqx_trans/
+ elim (lpxs_rneqg_inv_step_sn … H10 … Hn10) -H10 -Hn10
+ /3 width=8 by reqg_trans/
+| elim (lpxs_rneqg_inv_step_sn … HL10 … H) -HL10 -H // #L #K #HL1 #HnL1 #HLK #HKL0
+ elim (reqg_lpxs_trans … HLK0 … HKL0) -L0
+ /3 width=8 by lpxs_trans, reqg_trans/