Okay, officially reached my limit for errors due to term/type indices not matching up, am switching to the Calculus of Constructions.