#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2
/3 width=4 by lfxs_lref, tc_lfxs_step_dx, inj/
qed.
lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l.
#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2
/3 width=4 by lfxs_lref, tc_lfxs_step_dx, inj/
qed.
lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l.