initial subtype work
induction defined for subtype, started proving progress