interpretation "iterated extension on referred entries (local environment)"
'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2).
interpretation "iterated extension on referred entries (local environment)"
'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2).