module TelescopingLet5 where postulate A : Set a : A module B (a : A) where postulate C : Set -- B.C : (a : A) → Set module N = B a module M' (open N) (c : C) where postulate cc : C -- M.cc : (a : B.A a) → B.A a E = let open B a in C module M (open B a) (x : A) where D = C postulate cc : C -- M.cc : (a : B.A a) → B.A a