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