-include "basic_2/notation/relations/lazyeqsn_3.ma".
-
-definition ceq_ext: relation3 lenv bind bind ≝
- cext2 (λL,T1,T2. T1 = T2).
-
-definition lfeq: relation3 term lenv lenv ≝
- lfxs (λL,T1,T2. T1 = T2).
-
-interpretation
- "syntactic equivalence on referred entries (local environment)"
- 'LazyEqSn T L1 L2 = (lfeq T L1 L2).
-
-axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L →
- ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
-
-axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2.