/3 width=3 by lfxs_unit, inj/ qed.
lemma tc_lfxs_lref: ∀R,I,L1,L2,V1,V2,i.
- L1 ⪤**[R, #i] L2 â\86\92 L1.â\93\91{I}V1 ⪤**[R, #⫯i] L2.ⓑ{I}V2.
+ L1 ⪤**[R, #i] L2 â\86\92 L1.â\93\91{I}V1 ⪤**[R, #â\86\91i] L2.ⓑ{I}V2.
#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2
/3 width=4 by lfxs_lref, tc_lfxs_step_dx, inj/
qed.