(* Properties with syntactic equivalence on referred entries ****************)
-lemma lfeq_lfdeq: â\88\80h,o,L1,L2. â\88\80T:term. L1 â\89\90[T] L2 → L1 ≛[h, o, T] L2.
+lemma lfeq_lfdeq: â\88\80h,o,L1,L2. â\88\80T:term. L1 â\89¡[T] L2 → L1 ≛[h, o, T] L2.
/2 width=3 by lfxs_co/ qed.
-lemma lfeq_lfdeq_trans: â\88\80h,o,L1,L. â\88\80T:term. L1 â\89\90[T] L →
+lemma lfeq_lfdeq_trans: â\88\80h,o,L1,L. â\88\80T:term. L1 â\89¡[T] L →
∀L2. L ≛[h, o, T] L2 → L1 ≛[h, o, T] L2.
/2 width=3 by lfeq_lfxs_trans/ qed-.