scaffold for subst in lemma.
Restrict subst in lemma and prove bit of path case.

Restriction assumed OK.