  We prove the undecidability of the third order pattern matching problem in
typed lambda-calculi with dependent types and in those with type constructors
by reducing the second order unification problem to them.
