(* Basic_2A1: uses: lleq_dec *)
lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2).
/3 width=1 by lfxs_dec, tdeq_dec/ qed-.
(* Basic_2A1: uses: lleq_dec *)
lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2).
/3 width=1 by lfxs_dec, tdeq_dec/ qed-.