(* Inversion lemmas on negated lazy quivalence for local environments *******)
lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] L2 → ⊥) →
(* Inversion lemmas on negated lazy quivalence for local environments *******)
lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] L2 → ⊥) →