change membership rule to be like on paper. should be easier to induct on for subst lemma.