(* Properties on lazy equivalence for local environments ********************)
lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A →
(* Properties on lazy equivalence for local environments ********************)
lemma lleq_aaa_trans: ∀G,L2,T,A. ⦃G, L2⦄ ⊢ T ⁝ A →