(* Basic properties *********************************************************)
lemma eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
(* Basic properties *********************************************************)
lemma eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).