(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
-definition tc_lfxs (R): term → relation lenv ≝ LTC … (lfxs R).
+definition tc_lfxs (R): term → relation lenv ≝ CTC … (lfxs R).
interpretation "iterated extension on referred entries (local environment)"
'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2).
/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.