include "basic_2/syntax/ext2_ext2.ma".
include "basic_2/syntax/tdeq_tdeq.ma".
-include "basic_2/static/lfxs_lfxs.ma".
include "basic_2/static/lfdeq_length.ma".
(* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******)
(* Basic_2A1: uses: lleq_sym *)
lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T).
-/3 width=3 by lfdeq_fle_comp, lfxs_sym, tdeq_sym/ qed-.
+/3 width=3 by lfdeq_fsge_comp, lfxs_sym, tdeq_sym/ qed-.
(* Basic_2A1: uses: lleq_dec *)
lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2).