James C - Subst was broken. moves to inductive subst
James C - ready for proving again (sigh)
James C - necessary subst-uniqueness lemma
James C - using fake lemma for main proof
James C - new rename, rename lemma, better subst
James C - gahhh