/sci/ - Science & Math

Does subject reduction hold for a generic pure type system (not necessarily a member of the lambda cube)?
I've managed to reduce the problem to the base case [math]\Gamma \vdash (\lambda x:A.B)(t):C \implies \Gamma \vdash B[x:=t]:C[/math], and the usual recommended strategy is to induct on the structure of [math]B[/math], but I don't see how that helps prove even the simplest case [math]B=x[/math] without becoming circular.