bugfix in Lambda (base case for matching types)
allow to make variables polymorphic in Untyped structures
first attempt to make meta prover work again